--- a/src/Pure/Syntax/syntax.ML Sat Jan 27 16:45:27 2018 +0100
+++ b/src/Pure/Syntax/syntax.ML Sat Jan 27 16:56:03 2018 +0100
@@ -476,7 +476,7 @@
Syntax
({input = new_xprods @ input,
lexicon = fold Scan.extend_lexicon (Syntax_Ext.delims_of new_xprods) lexicon,
- gram = Lazy.value (Parser.extend_gram new_xprods (Lazy.force gram)),
+ gram = if null new_xprods then gram else Lazy.map (Parser.extend_gram new_xprods) gram,
consts = fold update_const consts2 consts1,
prmodes = insert (op =) mode prmodes,
parse_ast_trtab =