src/Pure/library.ML
changeset 20972 db0425645cc7
parent 20951 868120282837
child 21118 d9789a87825d
     1.1 --- a/src/Pure/library.ML	Wed Oct 11 10:49:29 2006 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Oct 11 10:49:36 2006 +0200
     1.3 @@ -219,10 +219,10 @@
     1.4    val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
     1.5    val \ : ''a list * ''a -> ''a list
     1.6    val \\ : ''a list * ''a list -> ''a list
     1.7 -  val findrep: ''a list -> ''a list
     1.8    val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
     1.9    val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
    1.10    val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
    1.11 +  val first_duplicate: ('a * 'a -> bool) -> 'a list -> 'a option
    1.12  
    1.13    (*lists as tables -- see also Pure/General/alist.ML*)
    1.14    val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
    1.15 @@ -1036,11 +1036,6 @@
    1.16  fun ys \\ xs = foldl (op \) (ys,xs);
    1.17  
    1.18  
    1.19 -(*returns the tail beginning with the first repeated element, or []*)
    1.20 -fun findrep [] = []
    1.21 -  | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
    1.22 -
    1.23 -
    1.24  (*makes a list of the distinct members of the input; preserves order, takes
    1.25    first of equal elements*)
    1.26  fun distinct eq lst =
    1.27 @@ -1068,6 +1063,11 @@
    1.28        | dups (x :: xs) = member eq xs x orelse dups xs;
    1.29    in dups end;
    1.30  
    1.31 +fun first_duplicate eq =
    1.32 +  let
    1.33 +    fun dup [] = NONE
    1.34 +      | dup (x :: xs) = if member eq xs x then SOME x else dup xs;
    1.35 +  in dup end;
    1.36  
    1.37  (** association lists -- legacy operations **)
    1.38