diff -r b7ee916ae3ec -r 4059413acbc1 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Dec 17 01:00:38 2005 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sat Dec 17 01:00:40 2005 +0100
@@ -278,7 +278,7 @@
     ({input = merge_lists' input1 input2,
       lexicon = Scan.merge_lexicons lexicon1 lexicon2,
       gram = Parser.merge_grams gram1 gram2,
-      consts = unique_strings (sort_strings (consts1 @ consts2)),
+      consts = sort_distinct string_ord (consts1 @ consts2),
       prmodes = merge_lists prmodes1 prmodes2,
       parse_ast_trtab =
         merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,