src/HOL/Library/Word.thy

--- a/src/HOL/Library/Word.thy	Wed Feb 17 10:00:22 2010 -0800
+++ b/src/HOL/Library/Word.thy	Wed Feb 17 10:30:36 2010 -0800
@@ -980,7 +980,8 @@
   fix xs
   assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)"
   thus "norm_signed (\<zero>#xs) = \<zero>#xs"
-    by (simp add: norm_signed_Cons norm_unsigned_equal split: split_if_asm)
+    by (simp add: norm_signed_Cons norm_unsigned_equal [THEN eqTrueI]
+             split: split_if_asm)
 next
   fix xs
   assume "length (norm_signed (\<one>#xs)) = Suc (length xs)"