# HG changeset patch
# User haftmann
# Date 1155017939 -7200
# Node ID d59364649bcc6b86958bdaab58b5dbd023b4c113
# Parent  1ffbe17cef3830071f6ab77f411be36b2c18e271
abandoned equal_list in favor for eq_list

diff -r 1ffbe17cef38 -r d59364649bcc NEWS
--- a/NEWS	Mon Aug 07 17:43:51 2006 +0200
+++ b/NEWS	Tue Aug 08 08:18:59 2006 +0200
@@ -552,6 +552,11 @@
 
 * Pure/library:
 
+Semantically identical functions "equal_list" and "eq_list" have been
+unified to "eq_list".
+
+* Pure/library:
+
   val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
   val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
 
diff -r 1ffbe17cef38 -r d59364649bcc src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Mon Aug 07 17:43:51 2006 +0200
+++ b/src/HOL/Algebra/ringsimp.ML	Tue Aug 08 08:18:59 2006 +0200
@@ -18,7 +18,7 @@
 (** Theory and context data **)
 
 fun struct_eq ((s1, ts1), (s2, ts2)) =
-  (s1 = s2) andalso equal_lists (op aconv) (ts1, ts2);
+  (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
 
 structure AlgebraData = GenericDataFun
 (struct
diff -r 1ffbe17cef38 -r d59364649bcc src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Aug 07 17:43:51 2006 +0200
+++ b/src/Pure/library.ML	Tue Aug 08 08:18:59 2006 +0200
@@ -142,7 +142,6 @@
   val filter: ('a -> bool) -> 'a list -> 'a list
   val filter_out: ('a -> bool) -> 'a list -> 'a list
   val map_filter: ('a -> 'b option) -> 'a list -> 'b list
-  val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
   val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
   val chop_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list)
@@ -568,6 +567,12 @@
 
 (* 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 maps f [] = []
   | maps f (x :: xs) = f x @ maps f xs;
 
@@ -646,10 +651,6 @@
             | SOME y => SOME (i, y)
   in get 0 end;
 
-fun eq_list _ ([], []) = true
-  | eq_list eq (x :: xs, y :: ys) = eq (x, y) andalso eq_list eq (xs, ys)
-  | eq_list _ _ = false;
-
 val flat = List.concat;
 
 fun unflat (xs :: xss) ys =
@@ -731,12 +732,6 @@
   [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
 val split_list = ListPair.unzip;
 
-fun equal_lists 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;
-
 
 (* prefixes, suffixes *)
 
@@ -1034,7 +1029,7 @@
 fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
 
 fun gen_eq_set eq (xs, ys) =
-  equal_lists eq (xs, ys) orelse
+  eq_list eq (xs, ys) orelse
     (gen_subset eq (xs, ys) andalso gen_subset (eq o swap) (ys, xs));
 
 
diff -r 1ffbe17cef38 -r d59364649bcc src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Aug 07 17:43:51 2006 +0200
+++ b/src/Pure/thm.ML	Tue Aug 08 08:18:59 2006 +0200
@@ -441,11 +441,11 @@
     Context.joinable (thy1, thy2) andalso
     Sorts.eq_set (shyps1, shyps2) andalso
     eq_set_hyps (hyps1, hyps2) andalso
-    equal_lists eq_tpairs (tpairs1, tpairs2) andalso
+    eq_list eq_tpairs (tpairs1, tpairs2) andalso
     prop1 aconv prop2
   end;
 
-val eq_thms = Library.equal_lists eq_thm;
+val eq_thms = eq_list eq_thm;
 
 fun theory_of_thm (Thm {thy_ref, ...}) = Theory.deref thy_ref;
 val sign_of_thm = theory_of_thm;