# HG changeset patch
# User haftmann
# Date 1160556576 -7200
# Node ID db0425645cc71d1a298c92a02cf1688de2d73de0
# Parent  1e7df197b8b818f581e7d6bf3a84bd4fda26920f
abandoned findrep

diff -r 1e7df197b8b8 -r db0425645cc7 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed Oct 11 10:49:29 2006 +0200
+++ b/src/HOL/Tools/meson.ML	Wed Oct 11 10:49:36 2006 +0200
@@ -273,8 +273,9 @@
 
 (*Remove duplicate literals, if there are any*)
 fun nodups th =
-    if null(findrep(literals(prop_of th))) then th
-    else nodups_aux [] th;
+  if has_duplicates (op =) (literals (prop_of th))
+    then nodups_aux [] th
+    else th;
 
 
 (**** Generation of contrapositives ****)
diff -r 1e7df197b8b8 -r db0425645cc7 src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Oct 11 10:49:29 2006 +0200
+++ b/src/Pure/library.ML	Wed Oct 11 10:49:36 2006 +0200
@@ -219,10 +219,10 @@
   val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val \ : ''a list * ''a -> ''a list
   val \\ : ''a list * ''a list -> ''a list
-  val findrep: ''a list -> ''a list
   val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
   val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
   val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
+  val first_duplicate: ('a * 'a -> bool) -> 'a list -> 'a option
 
   (*lists as tables -- see also Pure/General/alist.ML*)
   val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
@@ -1036,11 +1036,6 @@
 fun ys \\ xs = foldl (op \) (ys,xs);
 
 
-(*returns the tail beginning with the first repeated element, or []*)
-fun findrep [] = []
-  | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
-
-
 (*makes a list of the distinct members of the input; preserves order, takes
   first of equal elements*)
 fun distinct eq lst =
@@ -1068,6 +1063,11 @@
       | dups (x :: xs) = member eq xs x orelse dups xs;
   in dups end;
 
+fun first_duplicate eq =
+  let
+    fun dup [] = NONE
+      | dup (x :: xs) = if member eq xs x then SOME x else dup xs;
+  in dup end;
 
 (** association lists -- legacy operations **)
 
diff -r 1e7df197b8b8 -r db0425645cc7 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Wed Oct 11 10:49:29 2006 +0200
+++ b/src/Pure/meta_simplifier.ML	Wed Oct 11 10:49:36 2006 +0200
@@ -549,7 +549,7 @@
         Const ("==", _) $ lhs $ rhs =>
           let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
             is_Var x andalso forall is_Bound xs andalso
-            null (findrep xs) andalso xs = ys andalso
+            not (has_duplicates (op =) xs) andalso xs = ys andalso
             member (op =) varpairs (x, y) andalso
             is_full_cong_prems prems (remove (op =) (x, y) varpairs)
           end
@@ -561,7 +561,7 @@
     val (lhs, rhs) = Logic.dest_equals concl;
     val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
   in
-    f = g andalso null (findrep (xs @ ys)) andalso length xs = length ys andalso
+    f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso
     is_full_cong_prems prems (xs ~~ ys)
   end;
 
diff -r 1e7df197b8b8 -r db0425645cc7 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Oct 11 10:49:29 2006 +0200
+++ b/src/Pure/thm.ML	Wed Oct 11 10:49:36 2006 +0200
@@ -1376,9 +1376,9 @@
     val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
     val newBi = Logic.list_rename_params (newnames, Bi);
   in
-    case findrep cs of
-      c :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ c); state)
-    | [] =>
+    case first_duplicate (op =) cs of
+      SOME c => (warning ("Can't rename.  Bound variables not distinct: " ^ c); state)
+    | NONE =>
       (case cs inter_string freenames of
         a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); state)
       | [] =>