--- a/src/HOL/Library/Multiset_Order.thy Mon Jun 10 18:10:09 2024 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Mon Jun 10 21:32:24 2024 +0200
@@ -819,7 +819,7 @@
have "wfp ((<) :: 'a \<Rightarrow> 'a \<Rightarrow> bool)"
using wfp_on_less .
hence "wfp ((<) :: 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool)"
- unfolding less_multiset_def by (rule wfP_multp)
+ unfolding less_multiset_def by (rule wfp_multp)
thus "(\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P a"
unfolding wfp_on_def[of UNIV, simplified] by metis
qed