diff -r 316256709a8c -r 083eedb37a37 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 25 11:56:20 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 25 11:57:42 2011 -0700
@@ -792,7 +792,7 @@
  have "subspace ?P"
    by (auto simp add: subspace_def)
  ultimately show ?thesis
-   using x span_induct[of ?B ?P x] iS by blast
+   using x span_induct[of x ?B ?P] iS by blast
 qed
 
 lemma independent_stdbasis: "independent {cart_basis i ::real^'n |i. i\<in> (UNIV :: 'n set)}"