src/Pure/library.ML

--- a/src/Pure/library.ML	Fri Nov 26 23:14:14 2010 +0100
+++ b/src/Pure/library.ML	Sat Nov 27 00:00:54 2010 +0100
@@ -58,7 +58,6 @@
   val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
 
   (*lists*)
-  exception UnequalLengths
   val single: 'a -> 'a list
   val the_single: 'a list -> 'a
   val singleton: ('a list -> 'b list) -> 'a -> 'b
@@ -97,6 +96,7 @@
   val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   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 zip_options: 'a list -> 'b option list -> ('a * 'b) list
   val ~~ : 'a list * 'b list -> ('a * 'b) list
@@ -321,8 +321,6 @@
 
 (** lists **)
 
-exception UnequalLengths;
-
 fun single x = [x];
 
 fun the_single [x] = x
@@ -495,7 +493,7 @@
       let val (ps, qs) = chop (length xs) ys
       in ps :: unflat xss qs end
   | unflat [] [] = []
-  | unflat _ _ = raise UnequalLengths;
+  | unflat _ _ = raise ListPair.UnequalLengths;
 
 fun burrow f xss = unflat xss (f (flat xss));
 
@@ -534,19 +532,21 @@
 
 (* lists of pairs *)
 
-exception UnequalLengths;
-
 fun map2 _ [] [] = []
   | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys
-  | map2 _ _ _ = raise UnequalLengths;
+  | map2 _ _ _ = raise ListPair.UnequalLengths;
 
 fun fold2 f [] [] z = z
   | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
-  | fold2 f _ _ _ = raise UnequalLengths;
+  | fold2 f _ _ _ = raise ListPair.UnequalLengths;
+
+fun fold_rev2 f [] [] z = z
+  | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z)
+  | fold_rev2 f _ _ _ = raise ListPair.UnequalLengths;
 
 fun forall2 P [] [] = true
   | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
-  | forall2 P _ _ = raise UnequalLengths;
+  | forall2 P _ _ = raise ListPair.UnequalLengths;
 
 fun map_split f [] = ([], [])
   | map_split f (x :: xs) =
@@ -558,13 +558,13 @@
 fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys
   | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys
   | zip_options _ [] = []
-  | zip_options [] _ = raise UnequalLengths;
+  | zip_options [] _ = raise ListPair.UnequalLengths;
 
 (*combine two lists forming a list of pairs:
   [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
 fun [] ~~ [] = []
   | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
-  | _ ~~ _ = raise UnequalLengths;
+  | _ ~~ _ = raise ListPair.UnequalLengths;
 
 (*inverse of ~~; the old 'split':
   [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
@@ -843,10 +843,11 @@
 
 fun map_transpose f xss =
   let
-    val n = case distinct (op =) (map length xss)
-     of [] => 0
+    val n =
+      (case distinct (op =) (map length xss) of
+        [] => 0
       | [n] => n
-      | _ => raise UnequalLengths;
+      | _ => raise ListPair.UnequalLengths);
   in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end;
 
 
@@ -1066,3 +1067,5 @@
 
 structure Basic_Library: BASIC_LIBRARY = Library;
 open Basic_Library;
+
+datatype legacy = UnequalLengths;