--- 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
(