diff -r 31b9dfbe534c -r b10f7c981df6 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Mon Jun 10 13:44:46 2024 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Mon Jun 10 14:09:55 2024 +0200
@@ -715,7 +715,7 @@
 
 (** Termination rule **)
 
-val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}
+val wf_induct_rule = @{thm Wellfounded.wfp_induct_rule}
 val wf_in_rel = @{thm Fun_Def.wf_in_rel}
 val in_rel_def = @{thm Fun_Def.in_rel_def}