Made consts list operations a bit faster.
--- a/src/Pure/Syntax/syntax.ML Fri Aug 31 16:22:48 2001 +0200
+++ b/src/Pure/Syntax/syntax.ML Fri Aug 31 16:24:00 2001 +0200
@@ -208,8 +208,8 @@
lexicon = if inout then Scan.extend_lexicon lexicon (SynExt.delims_of xprods) else lexicon,
logtypes = extend_list logtypes1 logtypes2,
gram = if inout then Parser.extend_gram gram xprods else gram,
- consts = consts2 union consts1,
- prmodes = (mode ins prmodes2) union prmodes1,
+ consts = consts2 @ consts1,
+ prmodes = (mode ins prmodes2) union_string prmodes1,
parse_ast_trtab =
extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
parse_ruletab = extend_ruletab parse_ruletab parse_rules,
@@ -242,7 +242,7 @@
lexicon = Scan.merge_lexicons lexicon1 lexicon2,
logtypes = merge_lists logtypes1 logtypes2,
gram = Parser.merge_grams gram1 gram2,
- consts = merge_lists consts1 consts2,
+ consts = unique_strings (sort_strings (consts1 @ consts2)),
prmodes = merge_lists prmodes1 prmodes2,
parse_ast_trtab =
merge_trtabs parse_ast_trtab1 parse_ast_trtab2 "parse ast translation",