# HG changeset patch
# User wenzelm
# Date 1158055973 -7200
# Node ID 5e844572939db593433284c92f27c012066b5f94
# Parent  073a5ed7dd71b04441e3c1522a02ead074e55a1f
tuned eq_list;

diff -r 073a5ed7dd71 -r 5e844572939d src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Sep 12 12:12:46 2006 +0200
+++ b/src/Pure/library.ML	Tue Sep 12 12:12:53 2006 +0200
@@ -544,9 +544,9 @@
 (*  (op @) [x1, ..., xn]  ===>   x1 @ (x2 ... @ (x[n-1] @ xn))
     for n > 0, operators that associate to the right (not tail recursive)*)
 fun foldr1 f [] = raise Empty
-  | foldr1 f l = 
+  | foldr1 f l =
       let fun itr [x] = x
-	    | itr (x::l) = f(x, itr l)
+            | itr (x::l) = f(x, itr l)
       in  itr l  end;
 
 fun fold_index f =
@@ -568,11 +568,11 @@
 
 (* basic list functions *)
 
-fun eq_list eq (xs, ys) =
+fun eq_list eq (list1, list2) =
   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 eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys)
+      | eq_lst _ = true;
+  in length list1 = length list2 andalso eq_lst (list1, list2) end;
 
 fun maps f [] = []
   | maps f (x :: xs) = f x @ maps f xs;