diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Jun 27 22:08:55 2014 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Jun 28 09:16:42 2014 +0200
@@ -612,7 +612,7 @@
 
 lemma size_multiset_union [simp]:
   "size_multiset f (M + N::'a multiset) = size_multiset f M + size_multiset f N"
-apply (simp add: size_multiset_def setsum_Un_nat setsum_addf setsum_wcount_Int wcount_union)
+apply (simp add: size_multiset_def setsum_Un_nat setsum.distrib setsum_wcount_Int wcount_union)
 apply (subst Int_commute)
 apply (simp add: setsum_wcount_Int)
 done
@@ -2287,10 +2287,10 @@
   hence "?B = {b. h2 b = c \<and> ?As b \<noteq> {}}" by (auto simp add: setsum_gt_0_iff)
   hence A: "?A = \<Union> {?As b | b.  b \<in> ?B}" by auto
   have "setsum (count f) ?A = setsum (setsum (count f)) {?As b | b.  b \<in> ?B}"
-    unfolding A by transfer (intro setsum_Union_disjoint, auto simp: multiset_def)
+    unfolding A by transfer (intro setsum.Union_disjoint [simplified], auto simp: multiset_def setsum.Union_disjoint)
   also have "... = setsum (setsum (count f)) (?As ` ?B)" unfolding 0 ..
   also have "... = setsum (setsum (count f) o ?As) ?B"
-    by(intro setsum_reindex) (auto simp add: setsum_gt_0_iff inj_on_def)
+    by (intro setsum.reindex) (auto simp add: setsum_gt_0_iff inj_on_def)
   also have "... = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" unfolding comp_def ..
   finally have "setsum (count f) ?A = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" .
   thus "count (mmap (h2 \<circ> h1) f) c = count ((mmap h2 \<circ> mmap h1) f) c"
@@ -2300,7 +2300,7 @@
 lemma mmap_cong:
 assumes "\<And>a. a \<in># M \<Longrightarrow> f a = g a"
 shows "mmap f M = mmap g M"
-using assms by transfer (auto intro!: setsum_cong)
+using assms by transfer (auto intro!: setsum.cong)
 
 context
 begin
@@ -2458,7 +2458,7 @@
   (*  *)
   let ?ct1 = "N1 o e1"  let ?ct2 = "N2 o e2"
   have ss: "setsum ?ct1 {..<Suc n1} = setsum ?ct2 {..<Suc n2}"
-  unfolding setsum_reindex[OF e1_inj, symmetric] setsum_reindex[OF e2_inj, symmetric]
+  unfolding setsum.reindex[OF e1_inj, symmetric] setsum.reindex[OF e2_inj, symmetric]
   e1_surj e2_surj using ss .
   obtain ct where
   ct1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ?ct1 i1" and
@@ -2490,8 +2490,8 @@
     hence f1b1: "f1 b1 \<le> n1" using f1 unfolding bij_betw_def
     by (metis image_eqI lessThan_iff less_Suc_eq_le)
     have "(\<Sum>b2\<in>B2. M (u b1 b2)) = (\<Sum>i2<Suc n2. ct (f1 b1) (f2 (e2 i2)))"
-    unfolding e2_surj[symmetric] setsum_reindex[OF e2_inj]
-    unfolding M_def comp_def apply(intro setsum_cong) apply force
+    unfolding e2_surj[symmetric] setsum.reindex[OF e2_inj]
+    unfolding M_def comp_def apply(intro setsum.cong) apply force
     by (metis e2_surj b1 h1 h2 imageI)
     also have "... = N1 b1" using b1 ct1[OF f1b1] by simp
     finally show "(\<Sum>b2\<in>B2. M (u b1 b2)) = N1 b1" .
@@ -2500,8 +2500,8 @@
     hence f2b2: "f2 b2 \<le> n2" using f2 unfolding bij_betw_def
     by (metis image_eqI lessThan_iff less_Suc_eq_le)
     have "(\<Sum>b1\<in>B1. M (u b1 b2)) = (\<Sum>i1<Suc n1. ct (f1 (e1 i1)) (f2 b2))"
-    unfolding e1_surj[symmetric] setsum_reindex[OF e1_inj]
-    unfolding M_def comp_def apply(intro setsum_cong) apply force
+    unfolding e1_surj[symmetric] setsum.reindex[OF e1_inj]
+    unfolding M_def comp_def apply(intro setsum.cong) apply force
     by (metis e1_surj b2 h1 h2 imageI)
     also have "... = N2 b2" using b2 ct2[OF f2b2] by simp
     finally show "(\<Sum>b1\<in>B1. M (u b1 b2)) = N2 b2" .
@@ -2610,7 +2610,7 @@
   have set1_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set1 c \<inter> set1 c' = {}"
     unfolding set1_def by auto
   have setsum_set1: "\<And> c. setsum (count N1) (set1 c) = count P c"
-    unfolding P1 set1_def by transfer (auto intro: setsum_cong)
+    unfolding P1 set1_def by transfer (auto intro: setsum.cong)
 
   def set2 \<equiv> "\<lambda> c. {b2 \<in> set_of N2. f2 b2 = c}"
   have set2[simp]: "\<And> c b2. b2 \<in> set2 c \<Longrightarrow> f2 b2 = c" unfolding set2_def by auto
@@ -2625,7 +2625,7 @@
   have set2_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set2 c \<inter> set2 c' = {}"
     unfolding set2_def by auto
   have setsum_set2: "\<And> c. setsum (count N2) (set2 c) = count P c"
-    unfolding P2 set2_def by transfer (auto intro: setsum_cong)
+    unfolding P2 set2_def by transfer (auto intro: setsum.cong)
 
   have ss: "\<And> c. c \<in> set_of P \<Longrightarrow> setsum (count N1) (set1 c) = setsum (count N2) (set2 c)"
     unfolding setsum_set1 setsum_set2 ..
@@ -2746,9 +2746,9 @@
         have c: "c \<in> set_of P" and b1: "b1 \<in> set1 c"
           unfolding set1_def c_def P1 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
         with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p1 a = b1 \<and> a \<in> SET}"
-          by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
+          by transfer (force intro: setsum.mono_neutral_cong_left split: split_if_asm)
         also have "... = setsum (count M) ((\<lambda> b2. u c b1 b2) ` (set2 c))"
-          apply(rule setsum_cong) using c b1 proof safe
+          apply(rule setsum.cong) using c b1 proof safe
           fix a assume p1a: "p1 a \<in> set1 c" and "c \<in> set_of P" and "a \<in> SET"
           hence ac: "a \<in> sset c" using p1_rev by auto
           hence "a = u c (p1 a) (p2 a)" using c by auto
@@ -2756,10 +2756,10 @@
           ultimately show "a \<in> u c (p1 a) ` set2 c" by auto
         qed auto
         also have "... = setsum (\<lambda> b2. count M (u c b1 b2)) (set2 c)"
-          unfolding comp_def[symmetric] apply(rule setsum_reindex)
+          unfolding comp_def[symmetric] apply(rule setsum.reindex)
           using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast
         also have "... = count N1 b1" unfolding ss1[OF c b1, symmetric]
-          apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b1 set2)
+          apply(rule setsum.cong[OF refl]) apply (transfer fixing: Ms u c b1 set2)
           using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce
         finally show ?thesis .
       qed
@@ -2781,9 +2781,9 @@
         have c: "c \<in> set_of P" and b2: "b2 \<in> set2 c"
           unfolding set2_def c_def P2 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
         with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p2 a = b2 \<and> a \<in> SET}"
-          by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
+          by transfer (force intro: setsum.mono_neutral_cong_left split: split_if_asm)
         also have "... = setsum (count M) ((\<lambda> b1. u c b1 b2) ` (set1 c))"
-          apply(rule setsum_cong) using c b2 proof safe
+          apply(rule setsum.cong) using c b2 proof safe
           fix a assume p2a: "p2 a \<in> set2 c" and "c \<in> set_of P" and "a \<in> SET"
           hence ac: "a \<in> sset c" using p2_rev by auto
           hence "a = u c (p1 a) (p2 a)" using c by auto
@@ -2791,11 +2791,11 @@
           ultimately show "a \<in> (\<lambda>x. u c x (p2 a)) ` set1 c" by auto
         qed auto
         also have "... = setsum (count M o (\<lambda> b1. u c b1 b2)) (set1 c)"
-          apply(rule setsum_reindex)
+          apply(rule setsum.reindex)
           using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast
         also have "... = setsum (\<lambda> b1. count M (u c b1 b2)) (set1 c)" by simp
         also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def
-          apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b2 set1)
+          apply(rule setsum.cong[OF refl]) apply (transfer fixing: Ms u c b2 set1)
           using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce
         finally show ?thesis .
       qed
@@ -2855,7 +2855,7 @@
   assume "M1 \<in> multiset" "M2 \<in> multiset"
   hence "setsum M1 {a. f a = x \<and> 0 < M1 a} = setsum M1 {a. f a = x \<and> 0 < M1 a + M2 a}"
         "setsum M2 {a. f a = x \<and> 0 < M2 a} = setsum M2 {a. f a = x \<and> 0 < M1 a + M2 a}"
-    by (auto simp: multiset_def intro!: setsum_mono_zero_cong_left)
+    by (auto simp: multiset_def intro!: setsum.mono_neutral_cong_left)
   then show "(\<Sum>a | f a = x \<and> 0 < M1 a + M2 a. M1 a + M2 a) =
        setsum M1 {a. f a = x \<and> 0 < M1 a} +
        setsum M2 {a. f a = x \<and> 0 < M2 a}"
@@ -2897,7 +2897,7 @@
     by (metis (lifting, full_types) mem_Collect_eq neq0_conv setsum.neutral)
   have 0: "\<And> b. 0 < setsum (count M) (A b) \<longleftrightarrow> (\<exists> a \<in> A b. count M a > 0)"
   apply safe
-    apply (metis less_not_refl setsum_gt_0_iff setsum_infinite)
+    apply (metis less_not_refl setsum_gt_0_iff setsum.infinite)
     by (metis A_def finite_Collect_conjI finite_Collect_mem setsum_gt_0_iff)
   hence AB: "A ` ?B = {A b | b. \<exists> a \<in> A b. count M a > 0}" by auto