minor performance tuning (see also f906f7f83dae and b23c42b9f78a);
authorwenzelm
Tue, 09 May 2023 21:50:04 +0200
changeset 78010 6c2494750a4e
parent 78009 f906f7f83dae
child 78011 896e255d4fc4
minor performance tuning (see also f906f7f83dae and b23c42b9f78a);
src/Pure/Syntax/syntax.ML
--- 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