# HG changeset patch
# User wenzelm
# Date 1321283809 -3600
# Node ID 600682331b79f1f673b3fade6caadd2a80529f3b
# Parent  7a0975c9dd2666712b8467650db4fb6bb2b71370
more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers reset the trace (cf. Poly/ML SVN 1110);

diff -r 7a0975c9dd26 -r 600682331b79 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Mon Nov 14 12:29:19 2011 +0100
+++ b/src/Pure/Isar/runtime.ML	Mon Nov 14 16:16:49 2011 +0100
@@ -111,11 +111,8 @@
 (** controlled execution **)
 
 fun debugging f x =
-  if ! debug then
-    Exn.release (exception_trace (fn () =>
-      Exn.Res (f x) handle
-        exn as UNDEF => Exn.Exn exn
-      | exn as EXCURSION_FAIL _ => Exn.Exn exn))
+  if ! debug
+  then exception_trace (fn () => f x)
   else f x;
 
 fun controlled_execution f x =