src/HOL/Library/Multiset.thy

 instance
   by standard (simp add: equal_multiset_def)
 
 end
 
-lemma [code]: "sum_mset (mset xs) = sum_list xs"
-  by (induct xs) simp_all
+declare sum_mset_sum_list [code]
 
 lemma [code]: "prod_mset (mset xs) = fold times xs 1"
 proof -
   have "\<And>x. fold times xs x = prod_mset (mset xs) * x"
     by (induct xs) (simp_all add: ac_simps)