# HG changeset patch
# User wenzelm
# Date 1737977091 -3600
# Node ID e7c0bbbb819f2e97078375fcfba127d424c52c6c
# Parent  96afb07075323ffd398d76da74f4c799760b0fc6
more liberal type equivalence, following thys/Transport/HOL_Basics/Adhoc_Overloading/Adhoc_Overloading.thy from AFP/e69d71bc07c4;

diff -r 96afb0707532 -r e7c0bbbb819f 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
 (