changeset 66167 | 1bd268ab885c |
parent 64556 | 851ae0e7b09c |
child 67513 | 731b1ad6759a |
--- 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