# HG changeset patch
# User wenzelm
# Date 1683669400 -7200
# Node ID f5b67198b0194f504ddda8bd6e09f66f6743c136
# Parent  61c92140a6d29fc8e728a19bb692091efac9e579
backed out changeset 6c2494750a4e: it hardly makes a difference for heap size, but crashes arm64_32-darwin for unknown reasons;

diff -r 61c92140a6d2 -r f5b67198b019 src/Pure/Syntax/syntax.ML
--- 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