--- a/src/HOL/Tools/Transfer/transfer.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Sun Aug 04 17:39:47 2024 +0200
@@ -238,7 +238,7 @@
| is_eq _ = false
val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)
val eq_consts = rev (add_eqs t [])
- val eqTs = map (snd o dest_Const) eq_consts
+ val eqTs = map dest_Const_type eq_consts
val used = Term.add_free_names prop []
val names = map (K "") eqTs |> Name.variant_list used
val frees = map Free (names ~~ eqTs)
@@ -322,7 +322,7 @@
val prop = Thm.prop_of thm
val (t, mk_prop') = dest prop
val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])
- val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_tms
+ val Domainp_Ts = map (snd o dest_funT o dest_Const_type o fst o dest_comb) Domainp_tms
val used = Term.add_free_names t []
val rels = map (snd o dest_comb) Domainp_tms
val rel_names = map (fst o fst o dest_Var) rels