diff -r f5a77ee9106c -r e2d03448d5b5 src/HOL/Library/DAList_Multiset.thy
--- a/src/HOL/Library/DAList_Multiset.thy	Sun Feb 21 13:33:05 2021 +0100
+++ b/src/HOL/Library/DAList_Multiset.thy	Mon Feb 22 07:49:48 2021 +0000
@@ -100,7 +100,7 @@
 definition count_of :: "('a \<times> nat) list \<Rightarrow> 'a \<Rightarrow> nat"
   where "count_of xs x = (case map_of xs x of None \<Rightarrow> 0 | Some n \<Rightarrow> n)"
 
-lemma count_of_multiset: "count_of xs \<in> multiset"
+lemma count_of_multiset: "finite {x. 0 < count_of xs x}"
 proof -
   let ?A = "{x::'a. 0 < (case map_of xs x of None \<Rightarrow> 0::nat | Some n \<Rightarrow> n)}"
   have "?A \<subseteq> dom (map_of xs)"
@@ -117,7 +117,7 @@
   with finite_dom_map_of [of xs] have "finite ?A"
     by (auto intro: finite_subset)
   then show ?thesis
-    by (simp add: count_of_def fun_eq_iff multiset_def)
+    by (simp add: count_of_def fun_eq_iff)
 qed
 
 lemma count_simps [simp]:
@@ -291,7 +291,7 @@
   let ?inv = "{xs :: ('a \<times> nat) list. (distinct \<circ> map fst) xs}"
   note cs[simp del] = count_simps
   have count[simp]: "\<And>x. count (Abs_multiset (count_of x)) = count_of x"
-    by (rule Abs_multiset_inverse[OF count_of_multiset])
+    by (rule Abs_multiset_inverse) (simp add: count_of_multiset)
   assume ys: "ys \<in> ?inv"
   then show "fold_mset f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))"
     unfolding Bag_def unfolding Alist_inverse[OF ys]