# HG changeset patch
# User wenzelm
# Date 1704044940 -3600
# Node ID d9cf62ea273d8544f642dbf7ee972a6d3f69b77b
# Parent  c6c2e41cac1cb3c02fb5bca61f7a38d7e6d0f7cb
minor performance tuning: proper Same.operation;

diff -r c6c2e41cac1c -r d9cf62ea273d src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sun Dec 31 16:15:27 2023 +0100
+++ b/src/Pure/logic.ML	Sun Dec 31 18:49:00 2023 +0100
@@ -379,18 +379,16 @@
       map (fn (_, V) => (Type.sort_of_atyp V, V)) present_map @
       map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2;
 
-    fun atyp_operation {strip_sorts} T =
-      (case AList.lookup (op =) present_map T of
-        SOME U => U |> strip_sorts ? Type.strip_sorts
-      | NONE =>
-          (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of
-            SOME U => U |> strip_sorts ? Type.strip_sorts
-          | NONE => raise TYPE ("Dangling type variable ", [T], [prop])));
+    fun atyp_operation {strip_sorts} =
+      Same.function_eq (op =) (fn T =>
+        (case AList.lookup (op =) present_map T of
+          SOME T' => T' |> strip_sorts ? Type.strip_sorts
+        | NONE =>
+            (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of
+              SOME T' => T' |> strip_sorts ? Type.strip_sorts
+            | NONE => raise TYPE ("Dangling type variable ", [T], [prop]))));
 
-    fun typ_operation strip_sorts =
-      Term_Subst.map_atypsT_same (fn T =>
-        let val T' = atyp_operation strip_sorts T
-        in if T = T' then raise Same.SAME else T' end);
+    val typ_operation = Term_Subst.map_atypsT_same o atyp_operation;
 
     val constraints =
       constraints_map |> maps (fn (_, T as TVar (ai, S)) =>