# HG changeset patch
# User wenzelm
# Date 1695664165 -7200
# Node ID 72d2693fb0ecd61add4d1f16af9a0c87d67926a8
# Parent  0b794165e9d4a66fc15dc4cef5282783f4261e11
tuned: prefer antiquotation for try-finally;

diff -r 0b794165e9d4 -r 72d2693fb0ec src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Sep 25 19:28:14 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Sep 25 19:49:25 2023 +0200
@@ -279,7 +279,7 @@
          (output, run_time, used_from, atp_problem, tstplike_proof, atp_proof,
           atp_abduce_candidates, outcome),
          (format, type_enc)) =
-      with_cleanup clean_up run () |> tap export
+      \<^try>\<open>run () finally clean_up ()\<close> |> tap export
 
     val (outcome, used_facts, preferred_methss, message) =
       (case outcome of
diff -r 0b794165e9d4 -r 72d2693fb0ec src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Sep 25 19:28:14 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Sep 25 19:49:25 2023 +0200
@@ -12,7 +12,6 @@
   val plural_s : int -> string
   val serial_commas : string -> string list -> string list
   val simplify_spaces : string -> string
-  val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time : string -> string -> Time.time
   val subgoal_count : Proof.state -> int
@@ -42,11 +41,6 @@
 val serial_commas = Try.serial_commas
 val simplify_spaces = strip_spaces false (K true)
 
-fun with_cleanup clean_up f x =
-  Exn.capture f x
-  |> tap (fn _ => clean_up x)
-  |> Exn.release
-
 fun parse_bool_option option name s =
   (case s of
      "smart" => if option then NONE else raise Option.Option