--- a/src/HOL/Analysis/Lipschitz.thy Fri Apr 13 17:00:57 2018 +0100
+++ b/src/HOL/Analysis/Lipschitz.thy Sat Apr 14 09:23:00 2018 +0100
@@ -816,7 +816,7 @@
finally
have deriv: "\<forall>y\<in>cball x u. (f s has_derivative blinfun_apply (f' (s, y))) (at y within cball x u)"
using \<open>_ \<subseteq> X\<close>
- by (auto intro!: has_derivative_at_within[OF f'])
+ by (auto intro!: has_derivative_at_withinI[OF f'])
have "norm (f s y - f s z) \<le> B * norm (y - z)"
if "y \<in> cball x u" "z \<in> cball x u"
for y z