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)