--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Tue Feb 23 16:25:08 2016 +0100
@@ -387,7 +387,7 @@
have "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b
= (\<Sum>j\<in>Basis. if j = b then (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j))) else 0)"
using b
- by (auto simp add: algebra_simps inner_setsum_left inner_Basis split: split_if intro!: setsum.cong)
+ by (auto simp add: algebra_simps inner_setsum_left inner_Basis split: if_split intro!: setsum.cong)
also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))"
using b by (simp add: setsum.delta)
also have "\<dots> = f x \<bullet> b"