diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Binomial.thy	Fri May 13 20:24:10 2016 +0200
@@ -1324,7 +1324,7 @@
 proof -
   have "((m+r+k) choose (m+k)) * ((m+k) choose k) =
         fact (m+r + k) div (fact (m + k) * fact (m+r - m)) * (fact (m + k) div (fact k * fact m))"
-    by (simp add: assms binomial_altdef_nat)
+    by (simp add: binomial_altdef_nat)
   also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
     apply (subst div_mult_div_if_dvd)
     apply (auto simp: algebra_simps fact_fact_dvd_fact)