# HG changeset patch
# User wenzelm
# Date 1162759475 -3600
# Node ID 747ff99b35eed410c077d16d0e2a2757fdb3a823
# Parent  13c3fdccdf0d347bd1df20e956422acbe881cb1b
removed obsolete first_duplicate;

diff -r 13c3fdccdf0d -r 747ff99b35ee src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Nov 05 21:44:34 2006 +0100
+++ b/src/Pure/library.ML	Sun Nov 05 21:44:35 2006 +0100
@@ -220,7 +220,6 @@
   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
@@ -1051,11 +1050,6 @@
       | 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 13c3fdccdf0d -r 747ff99b35ee src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Nov 05 21:44:34 2006 +0100
+++ b/src/Pure/thm.ML	Sun Nov 05 21:44:35 2006 +0100
@@ -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 first_duplicate (op =) cs of
-      SOME c => (warning ("Can't rename.  Bound variables not distinct: " ^ c); state)
-    | NONE =>
+    (case duplicates (op =) cs of
+      a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); state)
+    | [] =>
       (case cs inter_string freenames of
         a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); state)
       | [] =>
@@ -1388,7 +1388,7 @@
           shyps = shyps,
           hyps = hyps,
           tpairs = tpairs,
-          prop = Logic.list_implies (Bs @ [newBi], C)})
+          prop = Logic.list_implies (Bs @ [newBi], C)}))
   end;