diff -r a7a5157c5e75 -r 052b348a98a9 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Thu Sep 28 16:01:48 2006 +0200
+++ b/src/HOL/Complex/Complex.thy	Thu Sep 28 19:04:13 2006 +0200
@@ -221,7 +221,7 @@
     by (simp add: complex_scaleR_def right_distrib)
   show "(a + b) *# x = a *# x + b *# x"
     by (simp add: complex_scaleR_def left_distrib [symmetric])
-  show "(a * b) *# x = a *# b *# x"
+  show "a *# b *# x = (a * b) *# x"
     by (simp add: complex_scaleR_def mult_assoc [symmetric])
   show "1 *# x = x"
     by (simp add: complex_scaleR_def complex_one_def [symmetric])