--- a/src/HOL/Binomial.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Binomial.thy Wed Aug 10 09:33:54 2016 +0200
@@ -317,7 +317,7 @@
text \<open>Another version of absorption, with \<open>-1\<close> instead of \<open>Suc\<close>.\<close>
lemma times_binomial_minus1_eq: "0 < k \<Longrightarrow> k * (n choose k) = n * ((n - 1) choose (k - 1))"
using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"]
- by (auto split add: nat_diff_split)
+ by (auto split: nat_diff_split)
subsection \<open>The binomial theorem (courtesy of Tobias Nipkow):\<close>