src/Pure/library.ML
changeset 21182 747ff99b35ee
parent 21118 d9789a87825d
child 21335 6b9d4a19a3a8
     1.1 --- a/src/Pure/library.ML	Sun Nov 05 21:44:34 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Sun Nov 05 21:44:35 2006 +0100
     1.3 @@ -220,7 +220,6 @@
     1.4    val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
     1.5    val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
     1.6    val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
     1.7 -  val first_duplicate: ('a * 'a -> bool) -> 'a list -> 'a option
     1.8  
     1.9    (*lists as tables -- see also Pure/General/alist.ML*)
    1.10    val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
    1.11 @@ -1051,11 +1050,6 @@
    1.12        | dups (x :: xs) = member eq xs x orelse dups xs;
    1.13    in dups end;
    1.14  
    1.15 -fun first_duplicate eq =
    1.16 -  let
    1.17 -    fun dup [] = NONE
    1.18 -      | dup (x :: xs) = if member eq xs x then SOME x else dup xs;
    1.19 -  in dup end;
    1.20  
    1.21  (** association lists -- legacy operations **)
    1.22