author | wenzelm |
Tue, 09 May 2023 23:56:40 +0200 | |
changeset 78013 | f5b67198b019 |
parent 78012 | 61c92140a6d2 |
child 78015 | 93f294ad42e6 |
--- a/src/Pure/Syntax/syntax.ML Tue May 09 23:12:09 2023 +0200 +++ b/src/Pure/Syntax/syntax.ML Tue May 09 23:56:40 2023 +0200 @@ -561,7 +561,7 @@ else let val input' = new_xprods2 @ input1; - val gram' = extend_gram new_xprods2 input1 gram1; + val gram' = new_gram input'; in (input', gram') end); in Syntax