src/HOL/Word/Word.thy
changeset 46645 573aff6b9b0a
parent 46618 a8c342aa53d6
child 46646 0abbf6dd09ee
--- 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