src/Pure/library.ML

   in  itr l  end;
 
 (*  (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 =
   let
     fun fold_aux _ [] y = y

   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 eq_list eq (list1, list2) =
+  let
+    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;
 
 fun chop 0 xs = ([], xs)