src/HOL/Library/DAList_Multiset.thy

     unfolding mset_less_eq_Bag0 by auto
 qed
 
 declare multiset_inter_def [code]
 declare sup_subset_mset_def [code]
-declare multiset_of.simps [code]
+declare mset.simps [code]
 
 
 fun fold_impl :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<times> nat) list \<Rightarrow> 'b"
 where
   "fold_impl fn e ((a,n) # ms) = (fold_impl fn ((fn a n) e) ms)"