--- 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,