diff -r 8c240fdeffcb -r 5840724b1d71 src/HOL/Library/ListVector.thy
--- a/src/HOL/Library/ListVector.thy	Sun Sep 23 21:49:31 2018 +0200
+++ b/src/HOL/Library/ListVector.thy	Mon Sep 24 14:30:09 2018 +0200
@@ -13,7 +13,7 @@
 text\<open>Multiplication with a scalar:\<close>
 
 abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70)
-where "x *\<^sub>s xs \<equiv> map (( * ) x) xs"
+where "x *\<^sub>s xs \<equiv> map ((*) x) xs"
 
 lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
 by (induct xs) simp_all