--- a/src/HOL/Multivariate_Analysis/Determinants.thy Tue Mar 18 11:58:30 2014 -0700
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Tue Mar 18 09:39:07 2014 -0700
@@ -964,7 +964,7 @@
by simp
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[OF fUk])
+ apply (rule span_setsum)
apply (rule ballI)
apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
apply (rule span_superset)