diff -r 183ea7f77b72 -r 1a2a53d03c31 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Apr 04 16:35:46 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Apr 04 21:35:59 2011 +0200
@@ -562,7 +562,7 @@
     Syntax
     ({input = input',
       lexicon = if changed then Scan.make_lexicon (Syn_Ext.delims_of input') else lexicon,
-      gram = if changed then Parser.make_gram input' else gram,
+      gram = if changed then Parser.extend_gram input' Parser.empty_gram else gram,
       consts = consts,
       prmodes = prmodes,
       parse_ast_trtab = remove_trtab (if_inout parse_ast_translation) parse_ast_trtab,