# HG changeset patch
# User wenzelm
# Date 1683661804 -7200
# Node ID 6c2494750a4e01a04b385900575f502b8d6af28d
# Parent  f906f7f83daee0ad369291978a2aebaa24e42d48
minor performance tuning (see also f906f7f83dae and b23c42b9f78a);

diff -r f906f7f83dae -r 6c2494750a4e 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