backed out changeset 6c2494750a4e: it hardly makes a difference for heap size, but crashes arm64_32-darwin for unknown reasons;
authorwenzelm
Tue, 09 May 2023 23:56:40 +0200
changeset 78013 f5b67198b019
parent 78012 61c92140a6d2
child 78015 93f294ad42e6
backed out changeset 6c2494750a4e: it hardly makes a difference for heap size, but crashes arm64_32-darwin for unknown reasons;
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