diff -r 7cf01ece66e4 -r dcfb33c26f50 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Tue Aug 05 16:21:27 2014 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Tue Aug 05 16:58:19 2014 +0200
@@ -249,7 +249,7 @@
 apply (simp (no_asm))
 (*induction step*)
 apply (subgoal_tac "(Suc (j+k) choose Suc k) > 0")
- prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
+ prefer 2 apply (simp, clarify)
 apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) = 
                     exponent p (Suc k)")
  txt{*First, use the assumed equation.  We simplify the LHS to
@@ -260,7 +260,7 @@
    @{text Suc_times_binomial_eq} ...*}
 apply (simp del: bad_Sucs add: Suc_times_binomial_eq [symmetric])
 txt{*...then @{text exponent_mult_add} and the quantified premise.*}
-apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add)
+apply (simp del: bad_Sucs add: exponent_mult_add)
 done
 
 (*The lemma above, with two changes of variables*)