# HG changeset patch
# User desharna
# Date 1740501846 -3600
# Node ID 6c2a087159b7d672fd1b34916042171abd489678
# Parent  a8e92f663481baa4730cffe06fcb501da1d8cbbc
tentatively catch Interrupt_Breakdown in Sledgehammer (from Jasmin)

diff -r a8e92f663481 -r 6c2a087159b7 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- 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
diff -r a8e92f663481 -r 6c2a087159b7 src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
--- 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