diff -r 16733b31e1cf -r 49c312eaaa11 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Wed Aug 02 13:48:21 2006 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Wed Aug 02 16:50:41 2006 +0200
@@ -326,7 +326,6 @@
 apply (subst times_binomial_minus1_eq, simp, simp)
 apply (subst exponent_mult_add, simp)
 apply (simp (no_asm_simp) add: zero_less_binomial_iff)
-apply arith
 apply (simp del: bad_Sucs add: exponent_mult_add const_p_fac_right)
 done