src/Pure/Isar/proof.ML

         writeln (Markup.markup Markup.state (Proof_Display.string_of_rule ctxt "Successful" th))
       else ();
     val test_proof =
       try (local_skip_proof true)
       |> Unsynchronized.setmp testing true
-      |> Exn.capture;
+      |> Exn.interruptible_capture;
 
     fun after_qed' results =
       refine_goals print_rule (context_of state) (flat results)
       #> check_result "Failed to refine any pending goal"
       #> after_qed results;

     |> 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 =>
-          if Exn.is_interrupt exn then reraise exn
-          else raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
+      | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
   end;
 
 in
 
 val have = gen_have (K I) ProofContext.bind_propp_i;