diff -r d022e8bd2375 -r cd05e9fcc63d src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Apr 08 21:01:59 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Apr 09 14:04:41 2013 +0200
@@ -1167,7 +1167,7 @@
 
 lemma differentiable_at_imp_differentiable_on:
   "(\<forall>x\<in>(s::(real^'n) set). f differentiable at x) \<Longrightarrow> f differentiable_on s"
-  unfolding differentiable_on_def by(auto intro!: differentiable_at_withinI)
+  by (metis differentiable_at_withinI differentiable_on_def)
 
 definition "jacobian f net = matrix(frechet_derivative f net)"