src/HOL/Library/Float.thy

   with floateq have a': "real a' = real a * pow2 (b - b')"
     by (simp add: pow2_diff field_simps)
 
   {
     assume bcmp: "b > b'"
-    then have "\<exists>c::nat. b - b' = int c + 1"
-      by arith
-    then guess c ..
+    then obtain c :: nat where "b - b' = int c + 1"
+      by atomize_elim arith
     with a' have "real a' = real (a * 2^c * 2)"
       by (simp add: pow2_def nat_add_distrib)
     with odd have False
       unfolding real_of_int_inject by simp
   }