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