adapt lemma mask_lem to respect int/bin distinction

--- a/src/HOL/Word/Bool_List_Representation.thy	Fri Feb 24 11:23:36 2012 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Feb 24 13:25:21 2012 +0100
@@ -681,13 +681,13 @@
   by (simp add : bl_to_bin_app_cat)
 
 lemma mask_lem: "(bl_to_bin (True # replicate n False)) = 
-    Int.succ (bl_to_bin (replicate n True))"
+    (bl_to_bin (replicate n True)) + 1"
   apply (unfold bl_to_bin_def)
   apply (induct n)
-   apply (simp add: Int.succ_def)
+   apply simp
   apply (simp only: Suc_eq_plus1 replicate_add
                     append_Cons [symmetric] bl_to_bin_aux_append)
-  apply (simp add: BIT_simps)
+  apply (simp add: Bit_B0_2t Bit_B1_2t)
   done
 
 (* function bl_of_nth *)

--- a/src/HOL/Word/Word.thy	Fri Feb 24 11:23:36 2012 +0100
+++ b/src/HOL/Word/Word.thy	Fri Feb 24 13:25:21 2012 +0100
@@ -3005,8 +3005,8 @@
   apply (unfold mask_def test_bit_bl)
   apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
   apply (clarsimp simp add: word_size)
-  apply (simp only: of_bl_no mask_lem number_of_succ add_diff_cancel2)
-  apply (fold of_bl_no)
+  apply (simp only: of_bl_def mask_lem word_of_int_hom_syms add_diff_cancel2)
+  apply (fold of_bl_def)
   apply (simp add: word_1_bl)
   apply (rule test_bit_of_bl [THEN trans, unfolded test_bit_bl word_size])
   apply auto