# HG changeset patch
# User wenzelm
# Date 1737978739 -3600
# Node ID c61434d8558eb113beae6bf73d2a7f077acc54c8
# Parent  e7c0bbbb819f2e97078375fcfba127d424c52c6c
tuned signature: more explicit Type.raw_equiv;

diff -r e7c0bbbb819f -r c61434d8558e src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Mon Jan 27 12:24:51 2025 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Mon Jan 27 12:52:19 2025 +0100
@@ -67,15 +67,14 @@
 fun wit_of_code_dt (CODE_DT code_dt) = #wit code_dt;
 fun wit_thm_of_code_dt (CODE_DT code_dt) = #wit_thm code_dt;
 fun rep_isom_data_of_code_dt (CODE_DT code_dt) = #rep_isom_data code_dt;
-fun ty_alpha_equiv (T, U) = Type.raw_instance (T, U) andalso Type.raw_instance (U, T);
-fun code_dt_eq c = (ty_alpha_equiv o apply2 rty_of_code_dt) c 
-  andalso (ty_alpha_equiv o apply2 qty_of_code_dt) c;
+fun code_dt_eq c = (Type.raw_equiv o apply2 rty_of_code_dt) c 
+  andalso (Type.raw_equiv o apply2 qty_of_code_dt) c;
 fun term_of_code_dt code_dt = code_dt |> `rty_of_code_dt ||> qty_of_code_dt |> HOLogic.mk_prodT
   |> Net.encode_type |> single;
 
 (* modulo renaming, typ must contain TVars *)
 fun is_code_dt_of_type (rty, qty) code_dt = code_dt |> `rty_of_code_dt ||> qty_of_code_dt
-  |> HOLogic.mk_prodT |> curry ty_alpha_equiv (HOLogic.mk_prodT (rty, qty));
+  |> HOLogic.mk_prodT |> curry Type.raw_equiv (HOLogic.mk_prodT (rty, qty));
 
 fun mk_rep_isom_data isom transfer bundle_name pointer =
   REP_ISOM { isom = isom, transfer = transfer, bundle_name = bundle_name, pointer = pointer}
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
 (
diff -r e7c0bbbb819f -r c61434d8558e src/Pure/type.ML
--- a/src/Pure/type.ML	Mon Jan 27 12:24:51 2025 +0100
+++ b/src/Pure/type.ML	Mon Jan 27 12:52:19 2025 +0100
@@ -84,6 +84,7 @@
   val could_match: typ * typ -> bool
   val could_matches: typ list * typ list -> bool
   val raw_instance: typ * typ -> bool
+  val raw_equiv: typ * typ -> bool
   exception TUNIFY
   val unify: tsig -> typ * typ -> tyenv * int -> tyenv * int
   val raw_unify: typ * typ -> tyenv -> tyenv
@@ -487,10 +488,11 @@
   | could_matches ([], []) = true
   | could_matches _ = false;
 
-fun raw_instance (T, U) =
-  if could_match (U, T) then
-    (Vartab.build (raw_match (U, T)); true) handle TYPE_MATCH => false
-  else false;
+fun can_raw_match arg =
+  (Vartab.build (raw_match arg); true) handle TYPE_MATCH => false;
+
+fun raw_instance (T, U) = could_match (U, T) andalso can_raw_match (U, T);
+fun raw_equiv (T, U) = could_match (U, T) andalso can_raw_match (U, T) andalso can_raw_match (T, U);
 
 
 (* unification *)