diff -r 8c240fdeffcb -r 5840724b1d71 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Sun Sep 23 21:49:31 2018 +0200
+++ b/src/HOL/Real.thy	Mon Sep 24 14:30:09 2018 +0200
@@ -32,7 +32,7 @@
   for x :: "'a::cancel_semigroup_add"
   by (meson add_left_imp_eq injI)
 
-lemma inj_mult_left [simp]: "inj (( * ) x) \<longleftrightarrow> x \<noteq> 0"
+lemma inj_mult_left [simp]: "inj ((*) x) \<longleftrightarrow> x \<noteq> 0"
   for x :: "'a::idom"
   by (metis injI mult_cancel_left the_inv_f_f zero_neq_one)