1.1 --- a/src/HOL/Library/Multiset.thy	Sat Jul 05 12:04:25 2014 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Sat Jul 05 16:04:23 2014 +0200
     1.3 @@ -1206,10 +1206,6 @@
     1.4    "setsum f A = msetsum (image_mset f (multiset_of_set A))"
     1.5    by (cases "finite A") (induct A rule: finite_induct, simp_all)
     1.6  
     1.7 -abbreviation msetsum_image :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b multiset \<Rightarrow> 'a"
     1.8 -where
     1.9 -  "msetsum_image f M \<equiv> msetsum (image_mset f M)"
    1.10 -
    1.11  end
    1.12  
    1.13  syntax
    1.14 @@ -1218,14 +1214,14 @@
    1.15  
    1.16  syntax (xsymbols)
    1.17    "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" 
    1.18 -      ("(3\<Sum>_:#_. _)" [0, 51, 10] 10)
    1.19 +      ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
    1.20  
    1.21  syntax (HTML output)
    1.22    "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" 
    1.23        ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
    1.24  
    1.25  translations
    1.26 -  "SUM i :# A. b" == "CONST msetsum_image (\<lambda>i. b) A"
    1.27 +  "SUM i :# A. b" == "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
    1.28  
    1.29  context comm_monoid_mult
    1.30  begin
    1.31 @@ -1262,10 +1258,6 @@
    1.32    "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_of M)"
    1.33    by (simp add: Multiset.fold_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
    1.34  
    1.35 -abbreviation msetprod_image :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b multiset \<Rightarrow> 'a"
    1.36 -where
    1.37 -  "msetprod_image f M \<equiv> msetprod (image_mset f M)"
    1.38 -
    1.39  end
    1.40  
    1.41  syntax
    1.42 @@ -1281,7 +1273,7 @@
    1.43        ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
    1.44  
    1.45  translations
    1.46 -  "PROD i :# A. b" == "CONST msetprod_image (\<lambda>i. b) A"
    1.47 +  "PROD i :# A. b" == "CONST msetprod (CONST image_mset (\<lambda>i. b) A)"
    1.48  
    1.49  lemma (in comm_semiring_1) dvd_msetprod:
    1.50    assumes "x \<in># A"