--- 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;