--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Tue Feb 25 17:44:01 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Tue Feb 25 17:44:06 2025 +0100
@@ -159,6 +159,7 @@
Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
HEADGOAL (tac_of_proof_method ctxt assmsp meth))
handle ERROR msg => error ("Preplay error: " ^ msg)
+ | Exn.Interrupt_Breakdown => error "Preplay error"
val play_outcome = take_time timeout prove ()
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Tue Feb 25 17:44:01 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Tue Feb 25 17:44:06 2025 +0100
@@ -113,6 +113,7 @@
HEADGOAL (tac_of ctxt name (local_facts, global_facts)));
NONE)
handle ERROR _ => SOME GaveUp
+ | Exn.Interrupt_Breakdown => SOME GaveUp
| Timeout.TIMEOUT _ => SOME TimedOut
val run_time = Timer.checkRealTimer timer