diff -r 08f3491c50bf -r 355a4cac5440 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Deriv.thy	Tue Sep 03 22:04:23 2013 +0200
@@ -1319,7 +1319,8 @@
     and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
     and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
     and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
-  shows "\<exists>g'c f'c c. DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
+  shows "\<exists>g'c f'c c.
+    DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
 proof -
   let ?h = "\<lambda>x. (f b - f a)*(g x) - (g b - g a)*(f x)"
   from assms have "a < b" by simp
@@ -1466,7 +1467,7 @@
     ultimately show "\<exists>y. 0 < y \<and> y < x \<and> f x / g x = f' y / g' y"
       using `f 0 = 0` `g 0 = 0` by (auto intro!: exI[of _ c])
   qed
-  then guess \<zeta> ..
+  then obtain \<zeta> where "\<forall>x\<in>{0 <..< a}. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)" ..
   then have \<zeta>: "eventually (\<lambda>x. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)) (at_right 0)"
     unfolding eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def)
   moreover
@@ -1582,9 +1583,10 @@
 
     have "\<exists>y. t < y \<and> y < a \<and> (g a - g t) * f' y = (f a - f t) * g' y"
       using f0 g0 t(1,2) by (intro GMVT') (force intro!: DERIV_isCont)+
-    then guess y ..
-    from this
-    have [arith]: "t < y" "y < a" and D_eq: "(f t - f a) / (g t - g a) = f' y / g' y"
+    then obtain y where [arith]: "t < y" "y < a"
+      and D_eq0: "(g a - g t) * f' y = (f a - f t) * g' y"
+      by blast
+    from D_eq0 have D_eq: "(f t - f a) / (g t - g a) = f' y / g' y"
       using `g a < g t` g'_neq_0[of y] by (auto simp add: field_simps)
 
     have *: "f t / g t - x = ((f t - f a) / (g t - g a) - x) * (1 - g a / g t) + (f a - x * g a) / g t"