diff -r e7c0bbbb819f -r c61434d8558e src/Pure/Tools/adhoc_overloading.ML
--- a/src/Pure/Tools/adhoc_overloading.ML	Mon Jan 27 12:24:51 2025 +0100
+++ b/src/Pure/Tools/adhoc_overloading.ML	Mon Jan 27 12:52:19 2025 +0100
@@ -58,12 +58,8 @@
 
 (* generic data *)
 
-fun type_eq pT =
-  let val matches = can (fn pT => Type.raw_match pT Vartab.empty)
-  in matches pT andalso matches (swap pT) end;
-
 fun variants_eq ((v1, T1), (v2, T2)) =
-  Term.aconv_untyped (v1, v2) andalso type_eq (T1, T2);
+  Term.aconv_untyped (v1, v2) andalso Type.raw_equiv (T1, T2);
 
 structure Overload_Data = Generic_Data
 (