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;