src/HOL/Analysis/Cauchy_Integral_Theorem.thy

       using g by auto
     have "vector_derivative g (at x within {0..1}) =
           vector_derivative (shiftpath (1 - a) (shiftpath a g)) (at x within {0..1})"
       apply (rule vector_derivative_at_within_ivl
                   [OF has_vector_derivative_transform_within_open
-                      [where f = "(shiftpath (1 - a) (shiftpath a g))" and s = "{0<..<1}-s"]])
+                      [where f = "(shiftpath (1 - a) (shiftpath a g))" and S = "{0<..<1}-s"]])
       using s g assms x
       apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath
                         vector_derivative_within_interior vector_derivative_works [symmetric])
       apply (rule differentiable_transform_within [OF gx, of "min x (1-x)"])
       apply (auto simp: dist_real_def shiftpath_shiftpath abs_if split: if_split_asm)

   have c: "continuous (at x within s) (\<lambda>w. if w = z then f' else (f w - f z) / (w - z))" if "x \<in> s" for x
   proof (cases "x = z")
     case True then show ?thesis
       apply (simp add: continuous_within)
       apply (rule Lim_transform_away_within [of _ "z+1" _ "\<lambda>w::complex. (f w - f z)/(w - z)"])
-      using has_field_derivative_at_within DERIV_within_iff f'
+      using has_field_derivative_at_within has_field_derivative_iff f'
       apply (fastforce simp add:)+
       done
   next
     case False
     then have dxz: "dist x z > 0" by auto

     apply (rule has_contour_integral_diff; rule has_contour_integral_div; simp add: field_simps; rule int)
     apply (metis contra_subsetD d dist_commute mem_ball that)
     apply (rule w)
     done
   show ?thes2
-    apply (simp add: DERIV_within_iff del: power_Suc)
+    apply (simp add: has_field_derivative_iff del: power_Suc)
     apply (rule Lim_transform_within [OF tendsto_mult_left [OF *] \<open>0 < d\<close> ])
     apply (simp add: \<open>k \<noteq> 0\<close> **)
     done
 qed