--- a/src/Pure/Isar/proof.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/Isar/proof.ML Thu Sep 09 17:20:27 2010 +0200
@@ -990,8 +990,9 @@
(case test_proof goal_state of
Exn.Result (SOME _) => goal_state
| Exn.Result NONE => error (fail_msg (context_of goal_state))
- | Exn.Exn Exn.Interrupt => raise Exn.Interrupt
- | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, 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))])))
end;
in