# HG changeset patch
# User wenzelm
# Date 1565723906 -7200
# Node ID bb18c7ac9cff8db2531659e135a815175de5b40b
# Parent  1615b6808192a7c4b0e388b3f61b129d69272b2b
minor performance tuning;

diff -r 1615b6808192 -r bb18c7ac9cff src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Aug 13 20:54:08 2019 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Aug 13 21:18:26 2019 +0200
@@ -549,15 +549,17 @@
       print_ast_trtab = print_ast_trtab2, prtabs = prtabs2} = tabs2;
 
     val (input', gram') =
-      (case subtract (op =) input1 input2 of
-        [] => (input1, gram1)
-      | new_xprods2 =>
-          if subset (op =) (input1, input2) then (input2, gram2)
-          else
-            let
-              val input' = new_xprods2 @ input1;
-              val gram' = Lazy.lazy_name "Syntax.merge_syntax" (fn () => Parser.make_gram input');
-            in (input', gram') end);
+      if pointer_eq (input1, input2) then (input1, gram1)
+      else
+        (case subtract (op =) input1 input2 of
+          [] => (input1, gram1)
+        | new_xprods2 =>
+            if subset (op =) (input1, input2) then (input2, gram2)
+            else
+              let
+                val input' = new_xprods2 @ input1;
+                val gram' = Lazy.lazy_name "Syntax.merge_syntax" (fn () => Parser.make_gram input');
+              in (input', gram') end);
   in
     Syntax
     ({input = input',