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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
