# HG changeset patch
# User paulson
# Date 1501794396 -7200
# Node ID ea6cbb69dda2c54082611d19547c3aeb0be16845
# Parent  604616b627f266d752843fe4e010a64bea7c335e# Parent  9786b06c7b5ad1d1a4fe67e6e6490d38156f35a2
merged

diff -r 9786b06c7b5a -r ea6cbb69dda2 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Aug 03 21:38:05 2017 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Aug 03 23:06:36 2017 +0200
@@ -3458,8 +3458,7 @@
 
 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 -