--- a/src/HOL/Binomial.thy Tue Mar 01 10:32:55 2016 +0100
+++ b/src/HOL/Binomial.thy Tue Mar 01 10:36:19 2016 +0100
@@ -697,9 +697,8 @@
then show ?thesis by simp
next
case False
- from this setprod_constant[of "{0 .. n - 1}" "- (1:: 'a)"]
- have eq: "(- (1::'a)) ^ n = setprod (\<lambda>i. - 1) {0 .. n - 1}"
- by auto
+ then have eq: "(- 1) ^ n = (\<Prod>i = 0..n - 1. - 1)"
+ by (auto simp add: setprod_constant)
from False show ?thesis
by (simp add: pochhammer_def gbinomial_def field_simps
eq setprod.distrib[symmetric])