--- 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