diff -r b3a5569a81e5 -r 07a7c2900877 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Mon May 14 08:15:13 2007 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Mon May 14 09:11:30 2007 +0200
@@ -550,7 +550,7 @@
        in summable_comparison_test)
 apply (rule_tac x = N in exI, safe)
 apply (drule le_Suc_ex_iff [THEN iffD1])
-apply (auto simp add: power_add realpow_not_zero)
+apply (auto simp add: power_add field_power_not_zero)
 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)