diff -r 1e246776f876 -r eb3dbbe971f6 src/HOL/Word/Num_Lemmas.thy
--- a/src/HOL/Word/Num_Lemmas.thy	Fri Apr 17 08:34:54 2009 +0200
+++ b/src/HOL/Word/Num_Lemmas.thy	Fri Apr 17 08:35:23 2009 +0200
@@ -66,7 +66,7 @@
   apply (safe dest!: even_equiv_def [THEN iffD1])
   apply (subst pos_zmod_mult_2)
    apply arith
-  apply (simp add: zmod_zmult_zmult1)
+  apply (simp add: mod_mult_mult1)
  done
 
 lemmas eme1p = emep1 [simplified add_commute]