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 *)