# HG changeset patch
# User wenzelm
# Date 1704747196 -3600
# Node ID 253d86888e84f1e92a95124ae44f3ea2bb662c12
# Parent  e83f5e3813b18c759eba1d7fd06b13c7350b7a9e
minor performance tuning;

diff -r e83f5e3813b1 -r 253d86888e84 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Jan 08 21:46:43 2024 +0100
+++ b/src/Pure/more_thm.ML	Mon Jan 08 21:53:16 2024 +0100
@@ -533,7 +533,9 @@
       map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S))))
         tfrees' tfrees;
     val strip = map (apply2 TFree) (tfrees ~~ tfrees');
-    val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t;
+    val t' =
+      (Term.map_types o Term.map_atyps_same)
+        (Same.function_eq (op =) (perhaps (AList.lookup (op =) strip))) t;
   in (strip, recover, t') end;
 
 fun add_axiom ctxt (b, prop) thy =