diff -r ad1ffcc90162 -r e96d5c42c4b0 src/HOL/NumberTheory/Int2.thy
--- a/src/HOL/NumberTheory/Int2.thy	Sat Feb 14 02:06:12 2004 +0100
+++ b/src/HOL/NumberTheory/Int2.thy	Sun Feb 15 10:46:37 2004 +0100
@@ -62,7 +62,7 @@
     by (auto simp add: zmod_zdiv_equality [THEN sym] zmult_ac)
   also assume  "x < y * z";
   finally show ?thesis;
-    by (auto simp add: prems zmult_zless_cancel2, insert prems, arith)
+    by (auto simp add: prems mult_less_cancel_right, insert prems, arith)
 qed;
 
 lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y";