[isabelle-dev] handle TYPE _

[Makarius]

On Wed, 15 Sep 2010, Walther Neuper wrote:

> Now a simple question, which might be caused by my missing experience of 
> how to handle Toplevel errors:
>
> 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".
>
> How are such type checks done nowadays ?

This is really just a plain type error: writeln produces (): unit, but the 
invocation of cterm_of a cterm.


> PS: I know that ctxt's are to be preferred to thy's; this will be done 
> in the next step of re-engineering.

cterm_of/ctyp_of is one of the very few points where a theory certificate 
appears in regular user-space code.  The typically you pass on 
certifiedness from one entity to another newly produced one.  Often the 
theory in question is obtain via Thm.theory_of_thm or Thm.theory_of_cterm.


 	Makarius