--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jan 31 19:16:41 2014 +0100
@@ -8,6 +8,7 @@
sig
val sledgehammerN : string
val log2 : real -> real
+ val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
val app_hd : ('a -> 'a) -> 'a list -> 'a list
val n_fold_cartesian_product : 'a list list -> 'a list list
val plural_s : int -> string
@@ -38,6 +39,8 @@
val log10_2 = Math.log10 2.0
fun log2 n = Math.log10 n / log10_2
+fun map3 xs = Ctr_Sugar_Util.map3 xs
+
fun app_hd f (x :: xs) = f x :: xs
fun cartesian_product [] _ = []