src/Pure/Tools/adhoc_overloading.ML

--- a/src/Pure/Tools/adhoc_overloading.ML	Mon Jan 27 12:13:37 2025 +0100
+++ b/src/Pure/Tools/adhoc_overloading.ML	Mon Jan 27 12:24:51 2025 +0100
@@ -58,8 +58,12 @@
 
 (* 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 T1 = T2;
+  Term.aconv_untyped (v1, v2) andalso type_eq (T1, T2);
 
 structure Overload_Data = Generic_Data
 (