tuned: prefer antiquotation for try-finally;

--- 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

--- 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