src/HOL/Complex.thy

--- a/src/HOL/Complex.thy	Thu Oct 31 16:54:22 2013 +0100
+++ b/src/HOL/Complex.thy	Fri Nov 01 18:51:14 2013 +0100
@@ -587,7 +587,7 @@
   by (simp add: cis_def)
 
 lemma cis_divide: "cis a / cis b = cis (a - b)"
-  by (simp add: complex_divide_def cis_mult diff_minus)
+  by (simp add: complex_divide_def cis_mult)
 
 lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
   by (auto simp add: DeMoivre)