diff -r e8ad51c88be9 -r f746af27164b src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Nov 03 17:55:55 1997 +0100
+++ b/src/Pure/library.ML	Mon Nov 03 17:56:39 1997 +0100
@@ -579,6 +579,20 @@
 
 fun distinct l = gen_distinct (op =) l;
 
+(*tuned version of distinct -- eq wrt. strings in fst component*)
+fun distinct_fst_string lst =
+  let
+    fun mem_str ((_:string, _), []) = false
+      | mem_str (p as (x, _), ((y, _) :: qs)) = x = y orelse mem_str (p, qs);
+
+    fun dist (rev_seen, []) = rev rev_seen
+      | dist (rev_seen, p :: ps) =
+          if mem_str (p, rev_seen) then dist (rev_seen, ps)
+          else dist (p :: rev_seen, ps);
+  in
+    dist ([], lst)
+  end;
+
 
 (*returns the tail beginning with the first repeated element, or []*)
 fun findrep [] = []