--- a/src/HOL/Number_Theory/Cong.thy Tue Mar 27 15:40:11 2012 +0200
+++ b/src/HOL/Number_Theory/Cong.thy Tue Mar 27 15:53:48 2012 +0200
@@ -214,9 +214,9 @@
lemma cong_mult_int:
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
apply (unfold cong_int_def)
- apply (subst (1 2) zmod_zmult1_eq)
+ apply (subst (1 2) mod_mult_right_eq)
apply (subst (1 2) mult_commute)
- apply (subst (1 2) zmod_zmult1_eq)
+ apply (subst (1 2) mod_mult_right_eq)
apply simp
done