src/Pure/library.ML
changeset 4496 16187138463d
parent 4479 708d7c26db5b
child 4616 d257e6c6614f
     1.1 --- a/src/Pure/library.ML	Sun Dec 28 15:47:09 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Dec 29 14:29:34 1997 +0100
     1.3 @@ -553,20 +553,6 @@
     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 [] = []