diff -r 31d41a0f6b5d -r 8e6cdb9c00a7 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Fri Sep 02 15:19:59 2011 -0700
+++ b/src/HOL/Library/Extended_Real.thy	Fri Sep 02 16:48:30 2011 -0700
@@ -1110,7 +1110,7 @@
     with `S \<noteq> {}` `\<infinity> \<notin> S` obtain x where "x \<in> S - {-\<infinity>}" "x \<noteq> \<infinity>" by auto
     with y `\<infinity> \<notin> S` have "\<forall>z\<in>real ` (S - {-\<infinity>}). z \<le> y"
       by (auto simp: real_of_ereal_ord_simps)
-    with reals_complete2[of "real ` (S - {-\<infinity>})"] `x \<in> S - {-\<infinity>}`
+    with complete_real[of "real ` (S - {-\<infinity>})"] `x \<in> S - {-\<infinity>}`
     obtain s where s:
        "\<forall>y\<in>S - {-\<infinity>}. real y \<le> s" "\<And>z. (\<forall>y\<in>S - {-\<infinity>}. real y \<le> z) \<Longrightarrow> s \<le> z"
        by auto