src/HOL/Library/Word.thy

--- a/src/HOL/Library/Word.thy	Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Library/Word.thy	Sat Jun 23 19:33:22 2007 +0200
@@ -443,7 +443,7 @@
           bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
           by simp
         also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
-          by (simp add: ring_distrib)
+          by (simp add: ring_distribs)
         finally show ?thesis .
       qed
     qed