--- a/src/HOL/Binomial.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Binomial.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -33,9 +33,8 @@
 by simp
 
 lemma binomial_eq_0 [rule_format]: "\<forall>k. n < k --> (n choose k) = 0"
-apply (induct "n", auto)
-apply (erule allE)
-apply (erule mp, arith)
+apply (induct "n")
+apply auto
 done
 
 declare binomial_0 [simp del] binomial_Suc [simp del]