diff -r a6047ddd9377 -r e4de7750cdeb src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Sep 01 07:31:33 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Sep 01 09:02:14 2011 -0700
@@ -1049,7 +1049,7 @@
   show ?thesis
     apply(rule has_derivative_inverse_basic_x[OF assms(6-8)])
     apply(rule continuous_on_interior[OF _ assms(3)])
-    apply(rule continuous_on_inverse[OF assms(4,1)])
+    apply(rule continuous_on_inv[OF assms(4,1)])
     apply(rule assms(2,5) assms(5)[rule_format] open_interior assms(3))+
     by(rule, rule *, assumption)
 qed