src/HOL/Presburger.thy

--- a/src/HOL/Presburger.thy	Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Presburger.thy	Tue Feb 10 12:02:11 2004 +0100
@@ -961,7 +961,7 @@
   apply (case_tac "0 \<le> k")
   apply rules
   apply (simp add: linorder_not_le)
-  apply (drule zmult_zless_mono2_neg [OF iffD2 [OF zero_less_int_conv]])
+  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   apply assumption
   apply (simp add: mult_ac)
   done