tuned eq_list;
authorwenzelm
Tue Sep 12 12:12:53 2006 +0200 (2006-09-12)
changeset 205105e844572939d
parent 20509 073a5ed7dd71
child 20511 c7daff0a3193
tuned eq_list;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Sep 12 12:12:46 2006 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Sep 12 12:12:53 2006 +0200
     1.3 @@ -544,9 +544,9 @@
     1.4  (*  (op @) [x1, ..., xn]  ===>   x1 @ (x2 ... @ (x[n-1] @ xn))
     1.5      for n > 0, operators that associate to the right (not tail recursive)*)
     1.6  fun foldr1 f [] = raise Empty
     1.7 -  | foldr1 f l = 
     1.8 +  | foldr1 f l =
     1.9        let fun itr [x] = x
    1.10 -	    | itr (x::l) = f(x, itr l)
    1.11 +            | itr (x::l) = f(x, itr l)
    1.12        in  itr l  end;
    1.13  
    1.14  fun fold_index f =
    1.15 @@ -568,11 +568,11 @@
    1.16  
    1.17  (* basic list functions *)
    1.18  
    1.19 -fun eq_list eq (xs, ys) =
    1.20 +fun eq_list eq (list1, list2) =
    1.21    let
    1.22 -    fun eq' [] [] = true
    1.23 -      | eq' (x :: xs) (y :: ys) = eq (x, y) andalso eq' xs ys
    1.24 -  in length xs = length ys andalso eq' xs ys end;
    1.25 +    fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys)
    1.26 +      | eq_lst _ = true;
    1.27 +  in length list1 = length list2 andalso eq_lst (list1, list2) end;
    1.28  
    1.29  fun maps f [] = []
    1.30    | maps f (x :: xs) = f x @ maps f xs;