# HG changeset patch
# User wenzelm
# Date 883402174 -3600
# Node ID 16187138463da2d3b0520f74e1d8d673d0fef7cf
# Parent  8648ba842d14db71c00c23a36f3fdc17c00a7235
removed distinct_fst_string;

diff -r 8648ba842d14 -r 16187138463d src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Dec 28 15:47:09 1997 +0100
+++ b/src/Pure/Syntax/syntax.ML	Mon Dec 29 14:29:34 1997 +0100
@@ -96,7 +96,7 @@
 (** tables of token translation functions **)
 
 fun lookup_tokentr tabs modes =
-  let val trs = distinct_fst_string (flat (map (assocs tabs) (modes @ [""])))
+  let val trs = gen_distinct eq_fst (flat (map (assocs tabs) (modes @ [""])))
   in fn c => apsome fst (assoc (trs, c)) end;
 
 fun merge_tokentrtabs tabs1 tabs2 =
diff -r 8648ba842d14 -r 16187138463d src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Sun Dec 28 15:47:09 1997 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Mon Dec 29 14:29:34 1997 +0100
@@ -436,7 +436,7 @@
 fun make_syntax keywords sects =
   let
     val dups = duplicates (map fst sects);
-    val sects' = distinct_fst_string sects;
+    val sects' = gen_distinct eq_fst sects;
   in
     if null dups then ()
     else warning ("Duplicate declaration of theory file sections:\n" ^ commas_quote dups);
diff -r 8648ba842d14 -r 16187138463d src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Dec 28 15:47:09 1997 +0100
+++ b/src/Pure/library.ML	Mon Dec 29 14:29:34 1997 +0100
@@ -553,20 +553,6 @@
 
 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 [] = []