src/HOL/Deriv.thy

--- a/src/HOL/Deriv.thy	Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Deriv.thy	Wed Apr 02 18:35:07 2014 +0200
@@ -1116,7 +1116,7 @@
 proof -
   let ?F = "%x. f x - ((f b - f a) / (b-a)) * x"
   have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x"
-    using con by (fast intro: isCont_intros)
+    using con by (fast intro: continuous_intros)
   have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable (at x)"
   proof (clarify)
     fix x::real