--- a/src/HOL/Hyperreal/FrechetDeriv.thy Tue Apr 17 00:33:49 2007 +0200
+++ b/src/HOL/Hyperreal/FrechetDeriv.thy Tue Apr 17 00:37:14 2007 +0200
@@ -67,8 +67,8 @@
apply (unfold_locales)
apply (simp only: f.add g.add add_ac)
apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
-apply (rule f.pos_boundedE, rename_tac Kf)
-apply (rule g.pos_boundedE, rename_tac Kg)
+apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
+apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
apply (rule_tac x="Kf + Kg" in exI, safe)
apply (subst right_distrib)
apply (rule order_trans [OF norm_triangle_ineq])