# HG changeset patch
# User wenzelm
# Date 1704021743 -3600
# Node ID 6bcb7131142d9be8b434ec29571f514a7dacd28e
# Parent  6e6f76c5dd96933f6cba2b42c479f653e9940eaa
minor performance tuning: proper Same.operation;

diff -r 6e6f76c5dd96 -r 6bcb7131142d src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Dec 31 11:50:05 2023 +0100
+++ b/src/Pure/thm.ML	Sun Dec 31 12:22:23 2023 +0100
@@ -1088,12 +1088,13 @@
 
         val types = present @ witnessed @ map (`Logic.dummy_tfree) extra';
         fun get_type S = types |> get_first (fn (T', S') => if le (S', S) then SOME T' else NONE);
-        fun map_atyp T =
-          if Types.defined present_set T then raise Same.SAME
-          else
-            (case get_type (Type.sort_of_atyp T) of
-              SOME T' => T'
-            | NONE => raise Fail "strip_shyps: bad type variable in proof term");
+        val map_atyp =
+          Same.function_eq (op =) (fn T =>
+            if Types.defined present_set T then raise Same.SAME
+            else
+              (case get_type (Type.sort_of_atyp T) of
+                SOME T' => T'
+              | NONE => raise Fail "strip_shyps: bad type variable in proof term"));
         val map_ztyp =
           ZTypes.unsynchronized_cache
             (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar));