src/Pure/Isar/proof.ML

     |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
     |> int ? (fn goal_state =>
       (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
 
 val have = gen_have (K I) ProofContext.bind_propp_i;