diff -r 82c20eaad94a -r be2e772e0adf src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Jun 10 08:25:55 2024 +0200
+++ b/src/HOL/Wellfounded.thy	Mon Jun 10 08:34:09 2024 +0200
@@ -1065,7 +1065,7 @@
     using convertible .
 qed
 
-lemma wfp_if_convertible_to_wfp: "wfP S \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> S (f x) (f y)) \<Longrightarrow> wfP R"
+lemma wfp_if_convertible_to_wfp: "wfp S \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> S (f x) (f y)) \<Longrightarrow> wfp R"
   using wf_if_convertible_to_wf[to_pred, of S R f] by simp
 
 text \<open>Converting to @{typ nat} is a very common special case that might be found more easily by
@@ -1073,7 +1073,7 @@
 
 lemma wfp_if_convertible_to_nat:
   fixes f :: "_ \<Rightarrow> nat"
-  shows "(\<And>x y. R x y \<Longrightarrow> f x < f y) \<Longrightarrow> wfP R"
+  shows "(\<And>x y. R x y \<Longrightarrow> f x < f y) \<Longrightarrow> wfp R"
   by (rule wfp_if_convertible_to_wfp[of "(<) :: nat \<Rightarrow> nat \<Rightarrow> bool", simplified])