1.1 --- a/src/HOL/Algebra/IntRing.thy	Mon Feb 16 19:35:52 2009 -0800
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Tue Feb 17 18:48:17 2009 +0100
     1.3 @@ -407,7 +407,7 @@
     1.4  
     1.5    hence "b mod m = (x * m + a) mod m" by simp
     1.6    also
     1.7 -      have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq)
     1.8 +      have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: mod_add_eq)
     1.9    also
    1.10        have "\<dots> = a mod m" by simp
    1.11    finally