src/HOL/Tools/Sledgehammer/sledgehammer_util.ML

   val log2 : real -> real
   val app_hd : ('a -> 'a) -> 'a list -> 'a list
   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
   val thms_in_proof : int -> (string Symtab.table * string Symtab.table) option -> thm ->
     string list option

 
 fun plural_s n = if n = 1 then "" else "s"
 
 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
    | "false" => SOME false