tuned;

--- a/src/Pure/General/timing.ML	Mon Mar 21 17:14:52 2011 +0100
+++ b/src/Pure/General/timing.ML	Mon Mar 21 20:15:03 2011 +0100
@@ -75,11 +75,9 @@
 fun cond_timeit enabled msg e =
   if enabled then
     let
-      val (timing, result) = timing (Exn.capture e) ();
+      val (timing, result) = timing (Exn.interruptible_capture e) ();
       val end_msg = message timing;
-      val _ =
-        if Exn.is_interrupt_exn result then ()
-        else warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
+      val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
     in Exn.release result end
   else e ();
 

--- a/src/Pure/Isar/proof.ML	Mon Mar 21 17:14:52 2011 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Mar 21 20:15:03 2011 +0100
@@ -999,7 +999,7 @@
     val test_proof =
       try (local_skip_proof true)
       |> Unsynchronized.setmp testing true
-      |> Exn.capture;
+      |> Exn.interruptible_capture;
 
     fun after_qed' results =
       refine_goals print_rule (context_of state) (flat results)
@@ -1012,9 +1012,7 @@
       (case test_proof goal_state of
         Exn.Result (SOME _) => goal_state
       | Exn.Result NONE => error (fail_msg (context_of goal_state))
-      | Exn.Exn exn =>
-          if Exn.is_interrupt exn then reraise exn
-          else raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
+      | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
   end;
 
 in