[isabelle-dev] AFP failure in Lam-ml-Normalization
jasmin.blanchette at gmail.com
Thu Nov 17 12:16:34 CET 2011
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
> 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".
More information about the isabelle-dev