--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu May 22 03:29:36 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu May 22 04:12:06 2014 +0200
@@ -10,7 +10,6 @@
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
val serial_commas : string -> string list -> string list
val simplify_spaces : string -> string
@@ -43,12 +42,6 @@
fun app_hd f (x :: xs) = f x :: xs
-fun cartesian_product [] _ = []
- | cartesian_product (x :: xs) yss =
- map (cons x) yss @ cartesian_product xs yss
-
-fun n_fold_cartesian_product xss = fold_rev cartesian_product xss [[]]
-
fun plural_s n = if n = 1 then "" else "s"
val serial_commas = Try.serial_commas