diff -r c7dfd924a165 -r 32b7eafc5a52 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Mar 18 11:58:30 2014 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Mar 18 09:39:07 2014 -0700
@@ -7057,10 +7057,7 @@
     fix i
     assume "i \<in> Basis" and "i \<notin> d"
     have "?a \<in> span d"
-      apply (rule span_setsum[of d "(\<lambda>b. b /\<^sub>R (2 * real (card d)))" d])
-      using finite_subset[OF assms(2) finite_Basis]
-      apply blast
-    proof -
+    proof (rule span_setsum[of d "(\<lambda>b. b /\<^sub>R (2 * real (card d)))" d])
       {
         fix x :: "'a::euclidean_space"
         assume "x \<in> d"