# HG changeset patch
# User wenzelm
# Date 1517068563 -3600
# Node ID 6877af8bc18dc643a8cd59a86f46f88f8ca9ded5
# Parent  731b1ad6759a6090c999a7946afb4a07e35cd9f8
prefer lazy update;

diff -r 731b1ad6759a -r 6877af8bc18d src/Pure/Syntax/syntax.ML
--- 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 =