changeset 82210 | 6c2a087159b7 |
parent 82209 | a8e92f663481 |
child 82212 | 0b46bf0a434f |
--- 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