1.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Sep 02 15:19:59 2011 -0700
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Sep 02 16:48:30 2011 -0700
     1.3 @@ -1110,7 +1110,7 @@
     1.4      with `S \<noteq> {}` `\<infinity> \<notin> S` obtain x where "x \<in> S - {-\<infinity>}" "x \<noteq> \<infinity>" by auto
     1.5      with y `\<infinity> \<notin> S` have "\<forall>z\<in>real ` (S - {-\<infinity>}). z \<le> y"
     1.6        by (auto simp: real_of_ereal_ord_simps)
     1.7 -    with reals_complete2[of "real ` (S - {-\<infinity>})"] `x \<in> S - {-\<infinity>}`
     1.8 +    with complete_real[of "real ` (S - {-\<infinity>})"] `x \<in> S - {-\<infinity>}`
     1.9      obtain s where s:
    1.10         "\<forall>y\<in>S - {-\<infinity>}. real y \<le> s" "\<And>z. (\<forall>y\<in>S - {-\<infinity>}. real y \<le> z) \<Longrightarrow> s \<le> z"
    1.11         by auto