1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -275,10 +275,10 @@
     1.4    apply clarify
     1.5    apply (elim pc_end pc_next pc_0)
     1.6    apply simp
     1.7 -  apply (fastsimp simp add: match_exception_entry_def sup_state_conv subcls1)
     1.8 +  apply (fastforce simp add: match_exception_entry_def sup_state_conv subcls1)
     1.9    apply simp
    1.10    apply simp
    1.11 -  apply (fastsimp simp add: sup_state_conv subcls1)
    1.12 +  apply (fastforce simp add: sup_state_conv subcls1)
    1.13    apply simp
    1.14    apply (simp add: app_def xcpt_app_def)
    1.15    apply simp