--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Jan 31 17:54:05 2013 +0100
@@ -11,6 +11,7 @@
val plural_s : int -> string
val serial_commas : string -> string list -> string list
val simplify_spaces : string -> string
+ val triple_self : ('a -> 'b) -> 'a * 'a * 'a -> 'b * 'b * 'b
val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
val infinite_timeout : Time.time
val time_mult : real -> Time.time -> Time.time
@@ -43,6 +44,8 @@
val serial_commas = Try.serial_commas
val simplify_spaces = strip_spaces false (K true)
+fun triple_self f (x, y, z) = (f x, f y, f z)
+
fun with_cleanup clean_up f x =
Exn.capture f x
|> tap (fn _ => clean_up x)