1.1 --- a/src/Pure/Syntax/syntax.ML	Mon Apr 19 17:57:07 2010 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Apr 19 23:11:39 2010 +0200
     1.3 @@ -290,15 +290,14 @@
     1.4      val SynExt.SynExt {xprods, consts = consts2, prmodes = prmodes2,
     1.5        parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
     1.6        print_ast_translation, token_translation} = syn_ext;
     1.7 -    val input' = if inout then fold (insert (op =)) xprods input else input;
     1.8 -    val changed = length input <> length input';
     1.9 +    val new_xprods =
    1.10 +      if inout then distinct (op =) (filter_out (member (op =) input) xprods) else [];
    1.11      fun if_inout xs = if inout then xs else [];
    1.12    in
    1.13      Syntax
    1.14 -    ({input = input',
    1.15 -      lexicon =
    1.16 -        if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
    1.17 -      gram = if changed then Parser.extend_gram gram xprods else gram,
    1.18 +    ({input = new_xprods @ input,
    1.19 +      lexicon = fold Scan.extend_lexicon (SynExt.delims_of new_xprods) lexicon,
    1.20 +      gram = Parser.extend_gram gram new_xprods,
    1.21        consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
    1.22        prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
    1.23        parse_ast_trtab =