diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/NthRoot.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -613,7 +613,7 @@
 apply (auto simp add: real_0_le_divide_iff power_divide)
 apply (rule_tac t = "u\<twosuperior>" in real_sum_of_halves [THEN subst])
 apply (rule add_mono)
-apply (auto simp add: four_x_squared simp del: realpow_Suc intro: power_mono)
+apply (auto simp add: four_x_squared intro: power_mono)
 done
 
 text "Legacy theorem names:"