--- a/src/HOL/NumberTheory/IntPrimes.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy Tue Feb 10 12:02:11 2004 +0100
@@ -338,7 +338,7 @@
a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
apply (unfold zcong_def dvd_def, auto)
apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong)
- apply (cut_tac z = a and w = b in zless_linear, auto)
+ apply (cut_tac x = a and y = b in linorder_less_linear, auto)
apply (subgoal_tac [2] "(a - b) mod m = a - b")
apply (rule_tac [3] mod_pos_pos_trivial, auto)
apply (subgoal_tac "(m + (a - b)) mod m = m + (a - b)")