diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Analysis/Generalised_Binomial_Theorem.thy
--- a/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -31,9 +31,9 @@
     let ?P = "\<Prod>i=0..<n. a - of_nat i"
     from n have "(a gchoose n) / (a gchoose Suc n) = (of_nat (Suc n) :: 'a) *
                    (?P / (\<Prod>i=0..n. a - of_nat i))"
-      by (simp add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
+      by (simp add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
     also from q have "(\<Prod>i=0..n. a - of_nat i) = ?P * (a - of_nat n)"
-      by (simp add: setprod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
+      by (simp add: prod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
     also have "?P / \<dots> = (?P / ?P) / (a - of_nat n)" by (rule divide_divide_eq_left[symmetric])
     also from assms have "?P / ?P = 1" by auto
     also have "of_nat (Suc n) * (1 / (a - of_nat n)) =
@@ -210,7 +210,7 @@
   also have "(of_real (1 + z) :: complex) powr (of_real a) = of_real ((1 + z) powr a)"
     using assms by (subst powr_of_real) simp_all
   also have "(of_real a gchoose n :: complex) = of_real (a gchoose n)" for n
-    by (simp add: gbinomial_setprod_rev)
+    by (simp add: gbinomial_prod_rev)
   hence "(\<lambda>n. (of_real a gchoose n :: complex) * of_real z ^ n) =
            (\<lambda>n. of_real ((a gchoose n) * z ^ n))" by (intro ext) simp
   finally show ?thesis by (simp only: sums_of_real_iff)