diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/IntDiv.thy	Sat Oct 20 12:09:33 2007 +0200
@@ -1339,7 +1339,7 @@
   apply simp
   apply (case_tac "0 \<le> k")
   apply iprover
-  apply (simp add: linorder_not_le)
+  apply (simp add: neq0_conv linorder_not_le)
   apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   apply assumption
   apply (simp add: mult_ac)