src/HOL/Real_Vector_Spaces.thy

 instance real :: linorder_topology
 proof
   show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
   proof (rule ext, safe)
     fix S :: "real set" assume "open S"
-    then guess f unfolding open_real_def bchoice_iff ..
+    then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)"
+      unfolding open_real_def bchoice_iff ..
     then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
       by (fastforce simp: dist_real_def)
     show "generate_topology (range lessThan \<union> range greaterThan) S"
       apply (subst *)
       apply (intro generate_topology_Union generate_topology.Int)

 proof (rule tendstoI)
   fix e :: real assume "0 < e"
   with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
     by (auto simp: LIMSEQ_def dist_real_def)
   { fix x :: real
-    from ex_le_of_nat[of x] guess n ..
+    obtain n where "x \<le> real_of_nat n"
+      using ex_le_of_nat[of x] ..
     note monoD[OF mono this]
     also have "f (real_of_nat n) \<le> y"
       by (rule LIMSEQ_le_const[OF limseq])
          (auto intro: exI[of _ n] monoD[OF mono] simp: real_eq_of_nat[symmetric])
     finally have "f x \<le> y" . }