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 =