src/HOL/Probability/Borel.thy

--- a/src/HOL/Probability/Borel.thy	Tue Feb 23 12:35:32 2010 -0800
+++ b/src/HOL/Probability/Borel.thy	Tue Feb 23 14:38:06 2010 -0800
@@ -82,7 +82,7 @@
     fix w n
     assume le: "f w \<le> g w - inverse(real(Suc n))"
     hence "0 < inverse(real(Suc n))"
-      by (metis inverse_real_of_nat_gt_zero)
+      by simp
     thus "f w < g w" using le
       by arith 
   qed