# HG changeset patch
# User wenzelm
# Date 1271711499 -7200
# Node ID 74c5e6e3c1d345ef543dadfe8c71b94b0e4bcb0a
# Parent  a94bbede91c77eaab5a88b017d4c6a48dfcf1ef2
update_syntax: add new productions only once, to allow repeated local notation, for example;

diff -r a94bbede91c7 -r 74c5e6e3c1d3 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Apr 19 17:57:07 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Apr 19 23:11:39 2010 +0200
@@ -290,15 +290,14 @@
     val SynExt.SynExt {xprods, consts = consts2, prmodes = prmodes2,
       parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
       print_ast_translation, token_translation} = syn_ext;
-    val input' = if inout then fold (insert (op =)) xprods input else input;
-    val changed = length input <> length input';
+    val new_xprods =
+      if inout then distinct (op =) (filter_out (member (op =) input) xprods) else [];
     fun if_inout xs = if inout then xs else [];
   in
     Syntax
-    ({input = input',
-      lexicon =
-        if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
-      gram = if changed then Parser.extend_gram gram xprods else gram,
+    ({input = new_xprods @ input,
+      lexicon = fold Scan.extend_lexicon (SynExt.delims_of new_xprods) lexicon,
+      gram = Parser.extend_gram gram new_xprods,
       consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
       prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
       parse_ast_trtab =