[isabelle-dev] handle TYPE _

[Tjark Weber]

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