# HG changeset patch
# User wenzelm
# Date 1704746786 -3600
# Node ID 6f2c3e4c97d72326562797e7082eb73a6272f116
# Parent  88341f610b3309e2f9091a9006574001fa3741a2
minor performance tuning;

diff -r 88341f610b33 -r 6f2c3e4c97d7 src/Pure/more_unify.ML
--- a/src/Pure/more_unify.ML	Mon Jan 08 21:30:21 2024 +0100
+++ b/src/Pure/more_unify.ML	Mon Jan 08 21:46:26 2024 +0100
@@ -34,13 +34,18 @@
         val pat_tvars = TVars.build (fold (TVars.add_tvars o #1) pairs');
         val pat_vars = Vars.build (fold (Vars.add_vars o #1) pairs');
 
-        val decr_indexesT =
-          Term.map_atyps (fn T as TVar ((x, i), S) =>
-            if i > maxidx then TVar ((x, i - offset), S) else T | T => T);
+        val decr_indexesT_same =
+          Term.map_atyps_same
+            (fn TVar ((x, i), S) =>
+                if i > maxidx then TVar ((x, i - offset), S) else raise Same.SAME
+              | _ => raise Same.SAME);
+        val decr_indexesT = Same.commit decr_indexesT_same;
         val decr_indexes =
-          Term.map_types decr_indexesT #>
-          Term.map_aterms (fn t as Var ((x, i), T) =>
-            if i > maxidx then Var ((x, i - offset), T) else t | t => t);
+          Term.map_types decr_indexesT_same #>
+          Term.map_aterms
+            (fn Var ((x, i), T) =>
+                if i > maxidx then Var ((x, i - offset), T) else raise Same.SAME
+              | _ => raise Same.SAME);
 
         fun norm_tvar env ((x, i), S) =
           let