diff -r abccf1b7ea4b -r 2c10c35dd4be src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Aug 10 15:56:48 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Aug 10 16:35:50 2011 -0700
@@ -1526,9 +1526,9 @@
 
 lemma has_derivative_vmul_component_cart: fixes c::"real^'a \<Rightarrow> real^'b" and v::"real^'c"
   assumes "(c has_derivative c') net"
-  shows "((\<lambda>x. c(x)$k *\<^sub>R v) has_derivative (\<lambda>x. (c' x)$k *\<^sub>R v)) net" 
-  using has_derivative_vmul_component[OF assms] 
-  unfolding nth_conv_component .
+  shows "((\<lambda>x. c(x)$k *\<^sub>R v) has_derivative (\<lambda>x. (c' x)$k *\<^sub>R v)) net"
+  unfolding nth_conv_component
+  by (intro has_derivative_intros assms)
 
 lemma differentiable_at_imp_differentiable_on: "(\<forall>x\<in>(s::(real^'n) set). f differentiable at x) \<Longrightarrow> f differentiable_on s"
   unfolding differentiable_on_def by(auto intro!: differentiable_at_withinI)
@@ -1641,8 +1641,6 @@
 lemma vec1_component[simp]: "(vec1 x)$1 = x"
   by (simp_all add:  vec_eq_iff)
 
-declare vec1_dest_vec1(1) [simp]
-
 lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
   by (metis vec1_dest_vec1(1))