src/Pure/Isar/runtime.ML

--- a/src/Pure/Isar/runtime.ML	Tue Feb 08 14:28:15 2011 +0100
+++ b/src/Pure/Isar/runtime.ML	Tue Feb 08 16:11:52 2011 +0100
@@ -106,10 +106,8 @@
       | exn as EXCURSION_FAIL _ => Exn.Exn exn))
   else f x;
 
-fun controlled_execution f =
-  f
-  |> debugging
-  |> Future.interruptible_task;
+fun controlled_execution f x =
+  ((f |> debugging |> Future.interruptible_task) x before Multithreading.interrupted ());
 
 fun toplevel_error output_exn f x = f x
   handle exn =>