--- a/src/HOL/Tools/Function/function_core.ML Fri Mar 22 10:38:35 2024 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Thu Mar 21 11:24:03 2024 +0100
@@ -780,7 +780,7 @@
val inrel_R = Const (\<^const_name>\<open>Fun_Def.in_rel\<close>,
HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
- val wfR' = HOLogic.mk_Trueprop (Const (\<^const_name>\<open>Wellfounded.wfP\<close>,
+ val wfR' = HOLogic.mk_Trueprop (Const (\<^const_abbrev>\<open>Wellfounded.wfP\<close>,
(domT --> domT --> boolT) --> boolT) $ R')
|> Thm.cterm_of ctxt' (* "wf R'" *)