--- a/src/HOL/Library/Extended_Real.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Library/Extended_Real.thy Fri Jan 08 17:40:59 2016 +0100
@@ -2769,7 +2769,7 @@
then have "open (ereal -` S)"
unfolding open_ereal_def by auto
with \<open>x \<in> S\<close> obtain r where "0 < r" and dist: "\<And>y. dist y rx < r \<Longrightarrow> ereal y \<in> S"
- unfolding open_real_def rx by auto
+ unfolding open_dist rx by auto
then obtain n where
upper: "\<And>N. n \<le> N \<Longrightarrow> u N < x + ereal r" and
lower: "\<And>N. n \<le> N \<Longrightarrow> x < u N + ereal r"