diff -r 8eb6365f5916 -r b9a1486e79be src/HOL/Library/Groups_Big_Fun.thy
--- a/src/HOL/Library/Groups_Big_Fun.thy	Sun Oct 16 22:43:51 2016 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Mon Oct 17 11:46:22 2016 +0200
@@ -216,11 +216,11 @@
 
 sublocale Sum_any: comm_monoid_fun plus 0
   defines Sum_any = Sum_any.G
-  rewrites "comm_monoid_set.F plus 0 = setsum"
+  rewrites "comm_monoid_set.F plus 0 = sum"
 proof -
   show "comm_monoid_fun plus 0" ..
   then interpret Sum_any: comm_monoid_fun plus 0 .
-  from setsum_def show "comm_monoid_set.F plus 0 = setsum" by (auto intro: sym)
+  from sum_def show "comm_monoid_set.F plus 0 = sum" by (auto intro: sym)
 qed
 
 end
@@ -240,7 +240,7 @@
   note assms
   moreover have "{a. g a * r \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
   ultimately show ?thesis
-    by (simp add: setsum_distrib_right Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
+    by (simp add: sum_distrib_right Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
 qed  
 
 lemma Sum_any_right_distrib:
@@ -251,7 +251,7 @@
   note assms
   moreover have "{a. r * g a \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
   ultimately show ?thesis
-    by (simp add: setsum_distrib_left Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
+    by (simp add: sum_distrib_left Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
 qed
 
 lemma Sum_any_product:
@@ -266,7 +266,7 @@
   ultimately show ?thesis using assms
     by (auto simp add: Sum_any.expand_set [of f] Sum_any.expand_set [of g]
       Sum_any.expand_superset [of "{a. f a \<noteq> 0}"] Sum_any.expand_superset [of "{b. g b \<noteq> 0}"]
-      setsum_product)
+      sum_product)
 qed
 
 lemma Sum_any_eq_zero_iff [simp]: 
@@ -325,7 +325,7 @@
   have "{a. c ^ f a \<noteq> 1} \<subseteq> {a. f a \<noteq> 0}"
     by (auto intro: ccontr)
   with assms show ?thesis
-    by (simp add: Sum_any.expand_set Prod_any.expand_superset power_setsum)
+    by (simp add: Sum_any.expand_set Prod_any.expand_superset power_sum)
 qed
 
 end