# HG changeset patch
# User wenzelm
# Date 878576155 -3600
# Node ID e8ad51c88be9360fc62709308f8ed6f468dd2dbb
# Parent  9f6907c40442f46060ae77585a3190698599876a
tuned: distinct_fst_string;

diff -r 9f6907c40442 -r e8ad51c88be9 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Nov 03 14:37:35 1997 +0100
+++ b/src/Pure/Syntax/syntax.ML	Mon Nov 03 17:55:55 1997 +0100
@@ -96,7 +96,7 @@
 (** tables of token translation functions **)
 
 fun lookup_tokentr tabs modes =
-  let val trs = gen_distinct eq_fst (flat (map (assocs tabs) (modes @ [""])))
+  let val trs = distinct_fst_string (flat (map (assocs tabs) (modes @ [""])))
   in fn c => apsome fst (assoc (trs, c)) end;
 
 fun merge_tokentrtabs tabs1 tabs2 =
diff -r 9f6907c40442 -r e8ad51c88be9 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Mon Nov 03 14:37:35 1997 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Mon Nov 03 17:55:55 1997 +0100
@@ -440,7 +440,7 @@
 fun make_syntax keywords sects =
   let
     val dups = duplicates (map fst sects);
-    val sects' = gen_distinct eq_fst sects;
+    val sects' = distinct_fst_string sects;
   in
     if null dups then ()
     else warning ("Duplicate declaration of theory file sections:\n" ^ commas_quote dups);
diff -r 9f6907c40442 -r e8ad51c88be9 src/Pure/name_space.ML
--- a/src/Pure/name_space.ML	Mon Nov 03 14:37:35 1997 +0100
+++ b/src/Pure/name_space.ML	Mon Nov 03 17:55:55 1997 +0100
@@ -72,8 +72,7 @@
           in
             map (rpair p o pack) (sfxs @ pfxs)
           end;
-    val mapping = filter_out (op =)
-      (gen_distinct eq_fst (flat (map accesses entries)));
+    val mapping = filter_out (op =) (distinct_fst_string (flat (map accesses entries)));
   in
     NameSpace (entries, Symtab.make mapping)
   end;