src/Pure/Isar/runtime.ML
changeset 39285 85728a4b5620
parent 39238 7189a138dd6c
child 39439 1c294d150ded
--- a/src/Pure/Isar/runtime.ML	Thu Sep 09 21:44:52 2010 +0200
+++ b/src/Pure/Isar/runtime.ML	Fri Sep 10 23:11:58 2010 +0200
@@ -34,7 +34,7 @@
 exception CONTEXT of Proof.context * exn;
 
 fun exn_context NONE exn = exn
-  | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn);
+  | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);
 
 
 (* exn_message *)