diff -r eb5d493a9e03 -r 60a42a4166af src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Mon May 09 16:02:23 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Mon May 09 17:23:19 2016 +0100
@@ -836,7 +836,6 @@
       unfolding thr0
       apply (rule span_setsum)
       apply simp
-      apply (rule ballI)
       apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
       apply (rule span_superset)
       apply auto
@@ -878,7 +877,6 @@
   have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A"
     apply (rule det_row_span)
     apply (rule span_setsum)
-    apply (rule ballI)
     apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
     apply (rule span_superset)
     apply auto