--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Sep 25 19:49:25 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Sep 25 20:56:44 2023 +0200
@@ -104,13 +104,10 @@
val birth = Timer.checkRealTimer timer
val filter_result as {outcome, ...} =
- SMT_Solver.smt_filter ctxt goal facts i run_timeout options
- handle exn =>
- if Exn.is_interrupt exn orelse debug then
- Exn.reraise exn
- else
- {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), fact_ids = NONE,
- atp_proof = K []}
+ \<^try>\<open>SMT_Solver.smt_filter ctxt goal facts i run_timeout options
+ catch exn =>
+ {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), fact_ids = NONE,
+ atp_proof = K []}\<close>
val death = Timer.checkRealTimer timer
val run_time = death - birth