diff -r 620db300c038 -r 57753e0ec1d4 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Sat Mar 21 12:37:13 2009 +0100
+++ b/src/HOL/Series.thy	Sun Mar 22 19:36:04 2009 +0100
@@ -557,7 +557,6 @@
 apply (induct_tac "na", auto)
 apply (rule_tac y = "c * norm (f (N + n))" in order_trans)
 apply (auto intro: mult_right_mono simp add: summable_def)
-apply (simp add: mult_ac)
 apply (rule_tac x = "norm (f N) * (1/ (1 - c)) / (c ^ N)" in exI)
 apply (rule sums_divide) 
 apply (rule sums_mult)