--- a/src/HOL/Complex.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Complex.thy Fri Nov 13 12:27:13 2015 +0000
@@ -842,7 +842,7 @@
by (simp add: cis_divide [symmetric] cis_2pi_int)
moreover have "- pi < c \<and> c \<le> pi"
using ceiling_correct [of "(b - pi) / (2*pi)"]
- by (simp add: c_def less_divide_eq divide_le_eq algebra_simps)
+ by (simp add: c_def less_divide_eq divide_le_eq algebra_simps del: le_of_int_ceiling)
ultimately show "\<exists>a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi" by fast
qed