diff -r 309c0a92e0da -r 295a8fc92684 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Fri Aug 29 07:43:25 2008 +0200
+++ b/src/HOL/Word/WordArith.thy	Fri Aug 29 08:14:58 2008 +0200
@@ -301,7 +301,7 @@
   by (auto simp: word_of_int_hom_syms [symmetric]
                  zadd_0_right add_commute add_assoc add_left_commute
                  mult_commute mult_assoc mult_left_commute
-                 plus_times.left_distrib plus_times.right_distrib)
+                 left_distrib right_distrib)
   
 lemmas word_add_ac = word_add_commute word_add_assoc word_add_left_commute
 lemmas word_mult_ac = word_mult_commute word_mult_assoc word_mult_left_commute