diff -r eb5d493a9e03 -r 60a42a4166af src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon May 09 16:02:23 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon May 09 17:23:19 2016 +0100
@@ -9,7 +9,7 @@
 
 lemma delta_mult_idempotent:
   "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)"
-  by (cases "k=a") auto
+  by simp
 
 lemma setsum_UNIV_sum:
   fixes g :: "'a::finite + 'b::finite \<Rightarrow> _"
@@ -812,7 +812,6 @@
       have "x \<in> span (columns A)"
         unfolding y[symmetric]
         apply (rule span_setsum)
-        apply clarify
         unfolding scalar_mult_eq_scaleR
         apply (rule span_mul)
         apply (rule span_superset)