src/HOL/Analysis/Linear_Algebra.thy

--- a/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 16 18:54:18 2019 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 16 16:50:35 2019 -0500
@@ -33,7 +33,7 @@
 
 subsection%unimportant \<open>More interesting properties of the norm\<close>
 
-notation inner (infix "\<bullet>" 70)
+unbundle inner_syntax
 
 text\<open>Equality of vectors in terms of \<^term>\<open>(\<bullet>)\<close> products.\<close>