diff -r 847e95ca9b0a -r 8e33b9d04a82 src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Wed Jun 30 16:28:13 2010 +0200
+++ b/src/HOL/Word/WordShift.thy	Wed Jun 30 16:28:13 2010 +0200
@@ -13,7 +13,7 @@
 subsection "Bit shifting"
 
 lemma shiftl1_number [simp] :
-  "shiftl1 (number_of w) = number_of (w BIT bit.B0)"
+  "shiftl1 (number_of w) = number_of (w BIT 0)"
   apply (unfold shiftl1_def word_number_of_def)
   apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm
               del: BIT_simps)
@@ -27,7 +27,7 @@
 
 lemmas shiftl1_def_u = shiftl1_def [folded word_number_of_def]
 
-lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT bit.B0)"
+lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT 0)"
   by (rule trans [OF _ shiftl1_number]) simp
 
 lemma shiftr1_0 [simp] : "shiftr1 0 = 0"