diff -r c88d1c36c9c3 -r 1bd268ab885c src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Thu Jun 22 14:27:13 2017 +0200 +++ b/src/Pure/Syntax/syntax.ML Thu Jun 22 15:20:32 2017 +0200 @@ -540,7 +540,7 @@ else let val input' = new_xprods2 @ input1; - val gram' = Lazy.lazy (fn () => Parser.make_gram input'); + val gram' = Lazy.lazy_name "Syntax.merge_syntax" (fn () => Parser.make_gram input'); in (input', gram') end); in Syntax