src/HOL/Analysis/Change_Of_Vars.thy

 proof -
   have "(\<lambda>x. \<bar>g' x\<bar> *\<^sub>R vec (f(g x)) :: real ^ 1) absolutely_integrable_on S \<and>
            integral S (\<lambda>x. \<bar>g' x\<bar> *\<^sub>R vec (f(g x))) = (vec b :: real ^ 1)
          \<longleftrightarrow> (\<lambda>x. vec (f x) :: real ^ 1) absolutely_integrable_on (g ` S) \<and>
            integral (g ` S) (\<lambda>x. vec (f x)) = (vec b :: real ^ 1)"
-    using assms unfolding has_field_derivative_iff_has_vector_derivative
+    using assms unfolding has_real_derivative_iff_has_vector_derivative
     by (intro has_absolute_integral_change_of_variables_1 assms) auto
   thus ?thesis
     by (simp add: absolutely_integrable_on_1_iff integral_on_1_eq)
 qed