src/Pure/Isar/proof.ML
changeset 39232 69c6d3e87660
parent 39129 976af4e27cde
child 39616 8052101883c3
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Sep 09 11:05:52 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Sep 09 17:20:27 2010 +0200
     1.3 @@ -990,8 +990,9 @@
     1.4        (case test_proof goal_state of
     1.5          Exn.Result (SOME _) => goal_state
     1.6        | Exn.Result NONE => error (fail_msg (context_of goal_state))
     1.7 -      | Exn.Exn Exn.Interrupt => raise Exn.Interrupt
     1.8 -      | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
     1.9 +      | Exn.Exn exn =>
    1.10 +          if Exn.is_interrupt exn then reraise exn
    1.11 +          else raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
    1.12    end;
    1.13  
    1.14  in