diff -r 31b9dfbe534c -r b10f7c981df6 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Jun 10 13:44:46 2024 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Jun 10 14:09:55 2024 +0200
@@ -1548,7 +1548,7 @@
 text \<open>Well-foundedness of strict subset relation\<close>
 
 lemma wf_subset_mset_rel: "wf {(M, N :: 'a multiset). M \<subset># N}"
-  using mset_subset_size wfP_def wfp_if_convertible_to_nat by blast
+  using mset_subset_size wfp_def wfp_if_convertible_to_nat by blast
 
 lemma wfP_subset_mset[simp]: "wfP (\<subset>#)"
   by (rule wf_subset_mset_rel[to_pred])
@@ -3246,7 +3246,7 @@
   unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
 
 lemma wfP_multp: "wfP r \<Longrightarrow> wfP (multp r)"
-  unfolding multp_def wfP_def
+  unfolding multp_def wfp_def
   by (simp add: wf_mult)