diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/NumberTheory/WilsonRuss.thy
--- a/src/HOL/NumberTheory/WilsonRuss.thy	Tue May 11 14:00:02 2004 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy	Tue May 11 20:11:08 2004 +0200
@@ -86,7 +86,7 @@
 
 lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
   apply (unfold zcong_def)
-  apply (simp add: Ring_and_Field.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
+  apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
   apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
    apply (simp add: mult_commute)
   apply (subst zdvd_zminus_iff)