--- a/src/HOL/NumberTheory/IntPrimes.thy Fri Aug 29 13:18:45 2003 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy Fri Aug 29 15:19:02 2003 +0200
@@ -400,7 +400,7 @@
lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
apply (unfold zcong_def)
apply (rule_tac t = "a - b" in ssubst)
- apply (rule_tac "m" = m in zcong_zmod_aux)
+ apply (rule_tac m = m in zcong_zmod_aux)
apply (rule trans)
apply (rule_tac [2] k = m and m = "a div m - b div m" in zdvd_reduce)
apply (simp add: zadd_commute)