[isabelle-dev] AFP failure in Lam-ml-Normalization

[Jasmin Blanchette]

Hi Makarius,

Am 17.11.2011 um 12:12 schrieb Makarius:

> This is merely a consequence of
> 
> changeset:   45486:600682331b79
> user:        wenzelm
> date:        Mon Nov 14 16:16:49 2011 +0100
> files:       src/Pure/Isar/runtime.ML
> description:
> more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers reset the trace (cf. Poly/ML SVN 1110);
> 
> It has the advantage that the exception trace becomes again more informative (as it used to be in Poly/ML 5.3), at the cost of some irrelevant traces about Toplevel.UNDEF, which is part of the normal operation of the Isar interpreter.

More informative traces are certainly a good thing. It's reassuring that it's not triggered by "metis".

Thanks,

Jasmin