diff -r 58ccbc73a172 -r a662e8139804 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Jul 14 12:21:12 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Jul 14 14:48:49 2016 +0100
@@ -2551,8 +2551,8 @@
   then have "cos (Arcsin z) \<noteq> 0"
     by (metis diff_0_right power_zero_numeral sin_squared_eq)
   then show ?thesis
-    apply (rule has_complex_derivative_inverse_basic [OF DERIV_sin])
-    apply (auto intro: isCont_Arcsin open_ball [of z 1] assms)
+    apply (rule has_complex_derivative_inverse_basic [OF DERIV_sin _ _ open_ball [of z 1]])
+    apply (auto intro: isCont_Arcsin assms)
     done
 qed
 
@@ -2716,8 +2716,8 @@
   then have "- sin (Arccos z) \<noteq> 0"
     by (metis cos_squared_eq diff_0_right mult_zero_left neg_0_equal_iff_equal power2_eq_square)
   then have "(Arccos has_field_derivative inverse(- sin(Arccos z))) (at z)"
-    apply (rule has_complex_derivative_inverse_basic [OF DERIV_cos])
-    apply (auto intro: isCont_Arccos open_ball [of z 1] assms)
+    apply (rule has_complex_derivative_inverse_basic [OF DERIV_cos _ _ open_ball [of z 1]])
+    apply (auto intro: isCont_Arccos assms)
     done
   then show ?thesis
     by simp