diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Complex.thy	Tue Sep 03 01:12:40 2013 +0200
@@ -707,11 +707,11 @@
       unfolding d_def by simp
     moreover from a assms have "cos a = cos x" and "sin a = sin x"
       by (simp_all add: complex_eq_iff)
-    hence "cos d = 1" unfolding d_def cos_diff by simp
-    moreover hence "sin d = 0" by (rule cos_one_sin_zero)
+    hence cos: "cos d = 1" unfolding d_def cos_diff by simp
+    moreover from cos have "sin d = 0" by (rule cos_one_sin_zero)
     ultimately have "d = 0"
       unfolding sin_zero_iff even_mult_two_ex
-      by (safe, auto simp add: numeral_2_eq_2 less_Suc_eq)
+      by (auto simp add: numeral_2_eq_2 less_Suc_eq)
     thus "a = x" unfolding d_def by simp
   qed (simp add: assms del: Re_sgn Im_sgn)
   with `z \<noteq> 0` show "arg z = x"