--- a/src/HOL/Tools/Transfer/transfer.ML Wed May 21 10:30:06 2025 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Wed May 21 10:30:07 2025 +0200
@@ -246,7 +246,7 @@
val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
val cprop = Thm.cterm_of ctxt prop2
- val equal_thm = Raw_Simplifier.rewrite ctxt false @{thms is_equality_lemma} cprop
+ val equal_thm = Raw_Simplifier.rewrite_wrt ctxt false @{thms is_equality_lemma} cprop
fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
in
forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
@@ -333,7 +333,7 @@
val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
val prop2 = Logic.list_rename_params (rev names) prop1
val cprop = Thm.cterm_of ctxt prop2
- val equal_thm = Raw_Simplifier.rewrite ctxt false @{thms Domainp_lemma} cprop
+ val equal_thm = Raw_Simplifier.rewrite_wrt ctxt false @{thms Domainp_lemma} cprop
fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
in
forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))