src/Pure/library.ML

   val multiply: 'a list -> 'a list list -> 'a list list
   val product: 'a list -> 'b list -> ('a * 'b) list
   val filter: ('a -> bool) -> 'a list -> 'a list
   val filter_out: ('a -> bool) -> 'a list -> 'a list
   val map_filter: ('a -> 'b option) -> 'a list -> 'b list
-  val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
   val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
   val chop_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list)
   val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
   val prefixes1: 'a list -> 'a list list

   in fold_aux end;
 
 
 (* basic list functions *)
 
+fun eq_list eq (xs, ys) =
+  let
+    fun eq' [] [] = true
+      | eq' (x :: xs) (y :: ys) = eq (x, y) andalso eq' xs ys
+  in length xs = length ys andalso eq' xs ys end;
+
 fun maps f [] = []
   | maps f (x :: xs) = f x @ maps f xs;
 
 fun chop 0 xs = ([], xs)
   | chop _ [] = ([], [])

       | get i (x :: xs) =
           case f x
            of NONE => get (i + 1) xs
             | SOME y => SOME (i, y)
   in get 0 end;
-
-fun eq_list _ ([], []) = true
-  | eq_list eq (x :: xs, y :: ys) = eq (x, y) andalso eq_list eq (xs, ys)
-  | eq_list _ _ = false;
 
 val flat = List.concat;
 
 fun unflat (xs :: xss) ys =
       let val (ps, qs) = chop (length xs) ys

   | _ ~~ _ = raise UnequalLengths;
 
 (*inverse of ~~; the old 'split':
   [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
 val split_list = ListPair.unzip;
-
-fun equal_lists eq (xs, ys) =
-  let
-    fun eq' [] [] = true
-      | eq' (x :: xs) (y :: ys) = eq (x, y) andalso eq' xs ys
-  in length xs = length ys andalso eq' xs ys end;
 
 
 (* prefixes, suffixes *)
 
 fun is_prefix _ [] _ = true

   xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
 
 fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
 
 fun gen_eq_set eq (xs, ys) =
-  equal_lists eq (xs, ys) orelse
+  eq_list eq (xs, ys) orelse
     (gen_subset eq (xs, ys) andalso gen_subset (eq o swap) (ys, xs));
 
 
 (*removing an element from a list WITHOUT duplicates*)
 fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)