On Wed, 2010-09-15 at 18:10 +0200, Walther Neuper wrote:
> I want to adapt code which tries to check types somehow as follows:
>
> ML {*
> Toplevel.debug := true;
> cterm_of @{theory} (@{term "a"} $ @{term "b"})
> handle TYPE _ => writeln "type error found";
> *}
>
> This results in the response buffer with:
>
> *** val it = () : unit
> *** Error (line 3):
> *** Can't unify cterm to {} (Incompatible types)
> *** Exception- ERROR "Static Errors" raised
> *** At command "ML".
cterm_of @{theory} (@{term "a"} $ @{term "b"}) is of type cterm, while
writeln "type error found" is of type {} (i.e., unit). This is not
allowed in SML: the type of the exception handler must be the same as
the type of the expression that could raise an exception.
Try
ML {*
Toplevel.debug := true;
ignore (cterm_of @{theory} (@{term "a"} $ @{term "b"}))
handle TYPE _ => writeln "type error found";
*}
Regards,
Tjark
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
