--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Tue Mar 15 08:34:04 2016 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Tue Mar 15 14:08:25 2016 +0000
@@ -613,7 +613,7 @@
then obtain r where "y = ennreal r"
by (cases y rule: ennreal_cases) auto
then show "\<exists>i\<in>UNIV. y < of_nat i"
- using ex_less_of_nat[of "max 1 r"] zero_less_one
+ using reals_Archimedean2[of "max 1 r"] zero_less_one
by (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_def less_ennreal.abs_eq eq_onp_def max.absorb2
dest!: one_less_of_natD intro: less_trans)
qed