--- a/src/HOL/Tools/Function/function_lib.ML Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML Wed Oct 08 17:09:07 2014 +0200
@@ -11,10 +11,6 @@
val dest_all_all: term -> term list * term
- val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
- val map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) -> 'a list -> 'b list -> 'c list ->
- 'd list -> 'e list -> 'f list -> 'g list -> 'h list
-
val unordered_pairs: 'a list -> ('a * 'a) list
val rename_bound: string -> term -> term
@@ -50,14 +46,6 @@
| dest_all_all t = ([],t)
-fun map4 f = Ctr_Sugar_Util.map4 f
-
-fun map7 _ [] [] [] [] [] [] [] = []
- | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs
- | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-
-
(* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
fun unordered_pairs [] = []
| unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs