diff -r 0c3a5e28f425 -r 8c5d10d41391 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Feb 23 15:23:16 2012 +0100
+++ b/src/HOL/Word/Word.thy	Thu Feb 23 15:37:42 2012 +0100
@@ -1102,7 +1102,7 @@
 lemma to_bl_0 [simp]:
   "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
   unfolding uint_bl
-  by (simp add : word_size bin_to_bl_Pls Pls_def [symmetric])
+  by (simp add: word_size bin_to_bl_zero)
 
 lemma uint_0_iff: "(uint x = 0) = (x = 0)"
   by (auto intro!: word_uint.Rep_eqD)