src/HOL/Library/Extended_Real.thy

   fix S
   assume "open S" and "x \<in> S"
   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"
     using assms(2)[of "ereal r"] by auto
   show "\<exists>N. \<forall>n\<ge>N. u n \<in> S"