--- a/src/HOL/Library/DAList_Multiset.thy Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Library/DAList_Multiset.thy Thu Mar 11 07:05:38 2021 +0000
@@ -200,7 +200,7 @@
lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<subseteq># m2 \<and> m2 \<subseteq># m1"
- by (metis equal_multiset_def subset_mset.eq_iff)
+ by (metis equal_multiset_def subset_mset.order_eq_iff)
text \<open>By default the code for \<open><\<close> is \<^prop>\<open>xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys\<close>.
With equality implemented by \<open>\<le>\<close>, this leads to three calls of \<open>\<le>\<close>.