src/HOL/Lim.thy

--- a/src/HOL/Lim.thy	Fri Aug 28 18:11:42 2009 +0200
+++ b/src/HOL/Lim.thy	Fri Aug 28 18:52:41 2009 +0200
@@ -544,8 +544,7 @@
     case True thus ?thesis using `0 < s` by auto
   next
     case False hence "s / 2 \<ge> (x - b) / 2" by auto
-    from inf_absorb2[OF this, unfolded inf_real_def]
-    have "?x = (x + b) / 2" by auto
+    hence "?x = (x + b) / 2" by(simp add:field_simps)
     thus ?thesis using `b < x` by auto
   qed
   hence "0 \<le> f ?x" using all_le `?x < x` by auto