diff -r d26a45f3c835 -r d12d89a66742 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 11 09:11:15 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 11 13:05:56 2011 -0700
@@ -467,7 +467,7 @@
 text {* some lemmas to map between Eucl and Cart *}
 lemma basis_real_n[simp]:"(basis (\<pi>' i)::real^'a) = cart_basis i"
   unfolding basis_vec_def using pi'_range[where 'n='a]
-  by (auto simp: vec_eq_iff)
+  by (auto simp: vec_eq_iff axis_def)
 
 subsection {* Orthogonality on cartesian products *}