1.1 --- a/src/Pure/Syntax/syntax.ML	Sat Dec 17 01:00:38 2005 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Dec 17 01:00:40 2005 +0100
     1.3 @@ -278,7 +278,7 @@
     1.4      ({input = merge_lists' input1 input2,
     1.5        lexicon = Scan.merge_lexicons lexicon1 lexicon2,
     1.6        gram = Parser.merge_grams gram1 gram2,
     1.7 -      consts = unique_strings (sort_strings (consts1 @ consts2)),
     1.8 +      consts = sort_distinct string_ord (consts1 @ consts2),
     1.9        prmodes = merge_lists prmodes1 prmodes2,
    1.10        parse_ast_trtab =
    1.11          merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,