src/Pure/Syntax/syntax.ML

         | new_xprods2 =>
             if subset (op =) (input1, input2) then (input2, gram2)
             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
     ({input = input',
       lexicon = Scan.merge_lexicons (lexicon1, lexicon2),