added distinct_fst_string;
authorwenzelm
Mon Nov 03 17:56:39 1997 +0100 (1997-11-03)
changeset 4102f746af27164b
parent 4101 e8ad51c88be9
child 4103 884968ad30da
added distinct_fst_string;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Mon Nov 03 17:55:55 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Nov 03 17:56:39 1997 +0100
     1.3 @@ -579,6 +579,20 @@
     1.4  
     1.5  fun distinct l = gen_distinct (op =) l;
     1.6  
     1.7 +(*tuned version of distinct -- eq wrt. strings in fst component*)
     1.8 +fun distinct_fst_string lst =
     1.9 +  let
    1.10 +    fun mem_str ((_:string, _), []) = false
    1.11 +      | mem_str (p as (x, _), ((y, _) :: qs)) = x = y orelse mem_str (p, qs);
    1.12 +
    1.13 +    fun dist (rev_seen, []) = rev rev_seen
    1.14 +      | dist (rev_seen, p :: ps) =
    1.15 +          if mem_str (p, rev_seen) then dist (rev_seen, ps)
    1.16 +          else dist (p :: rev_seen, ps);
    1.17 +  in
    1.18 +    dist ([], lst)
    1.19 +  end;
    1.20 +
    1.21  
    1.22  (*returns the tail beginning with the first repeated element, or []*)
    1.23  fun findrep [] = []