--- a/src/HOL/Analysis/Linear_Algebra.thy Thu May 03 15:07:14 2018 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Thu May 03 16:17:44 2018 +0200
@@ -917,7 +917,7 @@
and bg: "bilinear g"
and fg: "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> f i j = g i j"
shows "f = g"
- using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis] fg] by blast
+ using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg by blast
subsection \<open>Infinity norm\<close>