--- a/src/Pure/library.ML Wed Oct 08 17:09:07 2014 +0200
+++ b/src/Pure/library.ML Wed Oct 08 17:37:20 2014 +0200
@@ -101,8 +101,6 @@
val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
- val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
- val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
val zip_options: 'a list -> 'b option list -> ('a * 'b) list
val ~~ : 'a list * 'b list -> ('a * 'b) list
@@ -535,14 +533,6 @@
| fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
| fold2 _ _ _ _ = raise ListPair.UnequalLengths;
-fun fold_rev2 _ [] [] z = z
- | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z)
- | fold_rev2 _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun forall2 _ [] [] = true
- | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
- | forall2 _ _ _ = raise ListPair.UnequalLengths;
-
fun map_split _ [] = ([], [])
| map_split f (x :: xs) =
let