add type annotation

--- a/src/HOL/Hyperreal/MacLaurin.thy	Tue Dec 12 00:25:09 2006 +0100
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue Dec 12 04:31:34 2006 +0100
@@ -382,7 +382,7 @@
 
 lemma MVT2:
      "[| a < b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
-      ==> \<exists>z. a < z & z < b & (f b - f a = (b - a) * f'(z))"
+      ==> \<exists>z::real. a < z & z < b & (f b - f a = (b - a) * f'(z))"
 apply (drule MVT)
 apply (blast intro: DERIV_isCont)
 apply (force dest: order_less_imp_le simp add: differentiable_def)