diff -r d3d2b78b1c19 -r a8cc904a6820 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Complex.thy	Fri Oct 19 15:12:52 2012 +0200
@@ -141,7 +141,7 @@
 
 instance
   by intro_classes (simp_all add: complex_mult_def
-    right_distrib left_distrib right_diff_distrib left_diff_distrib
+    distrib_left distrib_right right_diff_distrib left_diff_distrib
     complex_inverse_def complex_divide_def
     power2_eq_square add_divide_distrib [symmetric]
     complex_eq_iff)
@@ -206,9 +206,9 @@
 proof
   fix a b :: real and x y :: complex
   show "scaleR a (x + y) = scaleR a x + scaleR a y"
-    by (simp add: complex_eq_iff right_distrib)
+    by (simp add: complex_eq_iff distrib_left)
   show "scaleR (a + b) x = scaleR a x + scaleR b x"
-    by (simp add: complex_eq_iff left_distrib)
+    by (simp add: complex_eq_iff distrib_right)
   show "scaleR a (scaleR b x) = scaleR (a * b) x"
     by (simp add: complex_eq_iff mult_assoc)
   show "scaleR 1 x = x"
@@ -297,7 +297,7 @@
        (simp add: real_sqrt_sum_squares_triangle_ineq)
   show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
     by (induct x)
-       (simp add: power_mult_distrib right_distrib [symmetric] real_sqrt_mult)
+       (simp add: power_mult_distrib distrib_left [symmetric] real_sqrt_mult)
   show "norm (x * y) = norm x * norm y"
     by (induct x, induct y)
        (simp add: real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
@@ -730,7 +730,7 @@
     unfolding z b_def rcis_def using `r \<noteq> 0`
     by (simp add: of_real_def sgn_scaleR sgn_if, simp add: cis_def)
   have cis_2pi_nat: "\<And>n. cis (2 * pi * real_of_nat n) = 1"
-    by (induct_tac n, simp_all add: right_distrib cis_mult [symmetric],
+    by (induct_tac n, simp_all add: distrib_left cis_mult [symmetric],
       simp add: cis_def)
   have cis_2pi_int: "\<And>x. cis (2 * pi * real_of_int x) = 1"
     by (case_tac x rule: int_diff_cases,