src/Pure/library.ML
changeset 19046 bc5c6c9b114e
parent 19011 d1c3294ca417
child 19119 dea8d858d37f
     1.1 --- a/src/Pure/library.ML	Wed Feb 15 19:11:10 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Feb 15 21:34:55 2006 +0100
     1.3 @@ -214,9 +214,8 @@
     1.4    val \\ : ''a list * ''a list -> ''a list
     1.5    val gen_rem: ('a * 'b -> bool) -> 'a list * 'b -> 'a list
     1.6    val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
     1.7 -  val gen_distinct: ('a * 'a -> bool) -> 'a list -> 'a list
     1.8 -  val distinct: ''a list -> ''a list
     1.9    val findrep: ''a list -> ''a list
    1.10 +  val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
    1.11    val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
    1.12    val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
    1.13  
    1.14 @@ -1011,24 +1010,20 @@
    1.15  fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
    1.16  fun gen_rems eq (xs, ys) = filter_out (member eq ys) xs;
    1.17  
    1.18 +(*returns the tail beginning with the first repeated element, or []*)
    1.19 +fun findrep [] = []
    1.20 +  | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
    1.21 +
    1.22 +
    1.23  (*makes a list of the distinct members of the input; preserves order, takes
    1.24    first of equal elements*)
    1.25 -fun gen_distinct eq lst =
    1.26 +fun distinct eq lst =
    1.27    let
    1.28      fun dist (rev_seen, []) = rev rev_seen
    1.29        | dist (rev_seen, x :: xs) =
    1.30            if member eq rev_seen x then dist (rev_seen, xs)
    1.31            else dist (x :: rev_seen, xs);
    1.32 -  in
    1.33 -    dist ([], lst)
    1.34 -  end;
    1.35 -
    1.36 -fun distinct l = gen_distinct (op =) l;
    1.37 -
    1.38 -(*returns the tail beginning with the first repeated element, or []*)
    1.39 -fun findrep [] = []
    1.40 -  | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
    1.41 -
    1.42 +  in dist ([], lst) end;
    1.43  
    1.44  (*returns a list containing all repeated elements exactly once; preserves
    1.45    order, takes first of equal elements*)