# HG changeset patch
# User wenzelm
# Date 1752239862 -7200
# Node ID d8ecaff223ff9b48ebfd72de2b986918531b1344
# Parent  c906b8df7bc3f9c76c5fc26f8b6cd926216551b5
minor performance tuning;

diff -r c906b8df7bc3 -r d8ecaff223ff src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Fri Jul 11 15:01:33 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Fri Jul 11 15:17:42 2025 +0200
@@ -93,10 +93,12 @@
 (
   type T = rules;
   val empty = make_rules Bires.empty_decls (Bires.kind_values Bires.empty_netpair) ([], []);
-  fun merge
-    (Rules {decls = decls1, netpairs = netpairs1, wrappers = (ws1, ws1')},
-     Rules {decls = decls2, netpairs = _, wrappers = (ws2, ws2')}) =
+  fun merge (rules1, rules2) =
+    if pointer_eq (rules1, rules2) then rules1
+    else
     let
+      val Rules {decls = decls1, netpairs = netpairs1, wrappers = (ws1, ws1')} = rules1;
+      val Rules {decls = decls2, netpairs = _, wrappers = (ws2, ws2')} = rules2;
       val (new_rules, decls) = Bires.merge_decls (decls1, decls2);
       val netpairs =
         netpairs1 |> map_index (uncurry (fn i =>