diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Transfer/transfer.ML
--- 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