author | wenzelm |
Tue, 09 May 2023 21:50:04 +0200 | |
changeset 78010 | 6c2494750a4e |
parent 78009 | f906f7f83dae |
child 78011 | 896e255d4fc4 |
--- a/src/Pure/Syntax/syntax.ML Tue May 09 21:32:03 2023 +0200 +++ b/src/Pure/Syntax/syntax.ML Tue May 09 21:50:04 2023 +0200 @@ -561,7 +561,7 @@ else let val input' = new_xprods2 @ input1; - val gram' = new_gram input'; + val gram' = extend_gram new_xprods2 input1 gram1; in (input', gram') end); in Syntax