src/Pure/library.ML

   val exists2: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val forall2: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val seq2: ('a * 'b -> unit) -> 'a list * 'b list -> unit
   val ~~ : 'a list * 'b list -> ('a * 'b) list
   val split_list: ('a * 'b) list -> 'a list * 'b list
+  val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val prefix: ''a list * ''a list -> bool
   val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
   val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
 
   (*integers*)

 
 (*inverse of ~~; the old 'split':
   [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
 fun split_list (l: ('a * 'b) list) = (map #1 l, map #2 l);
 
+fun equal_lists eq (xs, ys) = length xs = length ys andalso forall2 eq (xs, ys);
+
 
 (* prefixes, suffixes *)
 
 fun [] prefix _ = true
   | (x :: xs) prefix (y :: ys) = x = y andalso (xs prefix ys)