# HG changeset patch
# User haftmann
# Date 1133181836 -3600
# Node ID cbf6f44d73d349dab1d735804f24a73bcb191558
# Parent  6c2b039b4847f976c4064407acea84ed24a289e0
added (curried) fold2

diff -r 6c2b039b4847 -r cbf6f44d73d3 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Nov 28 10:58:40 2005 +0100
+++ b/src/Pure/library.ML	Mon Nov 28 13:43:56 2005 +0100
@@ -97,13 +97,14 @@
   val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
-  val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
+  val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
+  val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
-  val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+  val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
   val unflat: 'a list list -> 'b list -> 'b list list
   val splitAt: int * 'a list -> 'a list * 'a list
   val dropwhile: ('a -> bool) -> 'a list -> 'a list
-  val nth: 'a list -> int -> 'a 
+  val nth: 'a list -> int -> 'a
   val nth_update: int * 'a -> 'a list -> 'a list
   val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
   val split_last: 'a list -> 'a list * 'a
@@ -465,6 +466,13 @@
       | fold_aux (x :: xs) y = fold_aux xs (f x y);
   in fold_aux end;
 
+fun fold2 f =
+  let
+    fun fold_aux [] [] z = z
+      | fold_aux (x :: xs) (y :: ys) z = fold_aux xs ys (f x y z)
+      | fold_aux _ _ _ = raise UnequalLengths;
+  in fold_aux end;
+
 fun fold_rev f =
   let
     fun fold_aux [] y = y