diff -r 0a51765d2084 -r cdf12a1cb963 src/HOL/NumberTheory/IntPrimes.thy
--- a/src/HOL/NumberTheory/IntPrimes.thy	Mon Feb 16 19:35:52 2009 -0800
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Tue Feb 17 18:48:17 2009 +0100
@@ -88,7 +88,7 @@
 
 lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k) n = zgcd m n"
   apply (rule zgcd_eq [THEN trans])
-  apply (simp add: zmod_zadd1_eq)
+  apply (simp add: mod_add_eq)
   apply (rule zgcd_eq [symmetric])
   done