# HG changeset patch
# User berghofe
# Date 999267840 -7200
# Node ID 8d0c6543304875df6e03809e884b421ac44fa00f
# Parent  4db3876f1224c4c2b6e8fb01a305bfc0f7fda640
Made consts list operations a bit faster.

diff -r 4db3876f1224 -r 8d0c65433048 src/Pure/Syntax/syntax.ML
--- 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",