diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Library/Groups_Big_Fun.thy
--- a/src/HOL/Library/Groups_Big_Fun.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -283,11 +283,11 @@
 
 sublocale Prod_any: comm_monoid_fun times 1
   defines Prod_any = Prod_any.G
-  rewrites "comm_monoid_set.F times 1 = setprod"
+  rewrites "comm_monoid_set.F times 1 = prod"
 proof -
   show "comm_monoid_fun times 1" ..
   then interpret Prod_any: comm_monoid_fun times 1 .
-  from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym)
+  from prod_def show "comm_monoid_set.F times 1 = prod" by (auto intro: sym)
 qed
 
 end
@@ -308,7 +308,7 @@
   from \<open>f a = 0\<close> have "f a \<noteq> 1" by simp
   with \<open>f a = 0\<close> have "\<exists>a. f a \<noteq> 1 \<and> f a = 0" by blast
   with \<open>finite {a. f a \<noteq> 1}\<close> show ?thesis
-    by (simp add: Prod_any.expand_set setprod_zero)
+    by (simp add: Prod_any.expand_set prod_zero)
 qed
 
 lemma Prod_any_not_zero: