John Munroe wrote:
I'm wondering why the exception handling in the following doesn't behave what I expected to.
Goal.prove ctxt   goal1 (fn _ => auto_tac (clasimpset_of ctxt)) handle THM _ =>
[...]The Goal module catches the internal THM exception itself and re-raises it as a user error (exception ERROR). So the "handle THM _" does not catch it...