[isabelle-dev] handle TYPE _

[Walther Neuper]

While re-engineering ancient code I see that exception handling has 
changed in the last years. I see the many (* FIXME avoid handle _ *), 
the rules for exception handling within tactics in The Isabelle/Isar 
Implementation manual, suggestions for thread-safe handling etc.

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 ?

Walther

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