diff -r f64c715660c3 -r 8670a39d4420 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Sep 02 19:29:48 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Sep 02 13:57:12 2011 -0700
@@ -392,10 +392,10 @@
       proof (cases y)
         case (real r)
         with * have *: "\<And>i. f x i \<le> r * 2^i" by (auto simp: divide_le_eq)
-        from real_arch_lt[of r] * have "u x \<noteq> \<infinity>" by (auto simp: f_def) (metis less_le_not_le)
+        from reals_Archimedean2[of r] * have "u x \<noteq> \<infinity>" by (auto simp: f_def) (metis less_le_not_le)
         then have "\<exists>p. max 0 (u x) = ereal p \<and> 0 \<le> p" by (cases "u x") (auto simp: max_def)
         then guess p .. note ux = this
-        obtain m :: nat where m: "p < real m" using real_arch_lt ..
+        obtain m :: nat where m: "p < real m" using reals_Archimedean2 ..
         have "p \<le> r"
         proof (rule ccontr)
           assume "\<not> p \<le> r"