diff -r 7a5bbc2e4bad -r 8678986d9af5 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Jun 07 18:50:46 2024 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Jun 08 14:57:14 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])