diff -r c7dfd924a165 -r 32b7eafc5a52 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Mar 18 11:58:30 2014 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Mar 18 09:39:07 2014 -0700
@@ -467,11 +467,10 @@
 proof -
   let ?M = "(UNIV :: 'm set)"
   let ?N = "(UNIV :: 'n set)"
-  have fM: "finite ?M" by simp
   have "?rhs = (setsum (\<lambda>i.(x$i) *\<^sub>R f (axis i 1) ) ?M)$j"
     unfolding setsum_component by simp
   then show ?thesis
-    unfolding linear_setsum_mul[OF lf fM, symmetric]
+    unfolding linear_setsum_mul[OF lf, symmetric]
     unfolding scalar_mult_eq_scaleR[symmetric]
     unfolding basis_expansion
     by simp
@@ -674,7 +673,7 @@
         where y: "setsum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
       have "x \<in> span (columns A)"
         unfolding y[symmetric]
-        apply (rule span_setsum[OF fU])
+        apply (rule span_setsum)
         apply clarify
         unfolding scalar_mult_eq_scaleR
         apply (rule span_mul)