src/Pure/library.ML

   val \ : ''a list * ''a -> ''a list
   val \\ : ''a list * ''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
   val merge_lists: ''a list -> ''a list -> ''a list
   val merge_alists: (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list

   let
     fun dups [] = false
       | 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 **)
 
 fun gen_merge_lists _ xs [] = xs
   | gen_merge_lists _ [] ys = ys