1.1 --- a/src/HOL/Word/Word.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -655,7 +655,7 @@
     1.4  
     1.5  lemma to_bl_use_of_bl:
     1.6    "(to_bl w = bl) = (w = of_bl bl \<and> length bl = length (to_bl w))"
     1.7 -  by (fastsimp elim!: word_bl.Abs_inverse [simplified])
     1.8 +  by (fastforce elim!: word_bl.Abs_inverse [simplified])
     1.9  
    1.10  lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
    1.11    unfolding word_reverse_def by (simp add: word_bl.Abs_inverse)
    1.12 @@ -3702,7 +3702,7 @@
    1.13    apply (case_tac "word_split c")
    1.14    apply (frule test_bit_split)
    1.15    apply (erule trans)
    1.16 -  apply (fastsimp intro ! : word_eqI simp add : word_size)
    1.17 +  apply (fastforce intro ! : word_eqI simp add : word_size)
    1.18    done
    1.19  
    1.20  -- {* this odd result is analogous to @{text "ucast_id"},