--- a/src/HOL/MicroJava/BV/BVExample.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Mon Sep 12 07:55:43 2011 +0200
@@ -275,10 +275,10 @@
apply clarify
apply (elim pc_end pc_next pc_0)
apply simp
- apply (fastsimp simp add: match_exception_entry_def sup_state_conv subcls1)
+ apply (fastforce simp add: match_exception_entry_def sup_state_conv subcls1)
apply simp
apply simp
- apply (fastsimp simp add: sup_state_conv subcls1)
+ apply (fastforce simp add: sup_state_conv subcls1)
apply simp
apply (simp add: app_def xcpt_app_def)
apply simp