--- a/src/HOL/MicroJava/J/WellForm.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Mon Sep 12 07:55:43 2011 +0200
@@ -314,7 +314,7 @@
apply( frule class_Object)
apply( clarify)
apply( frule fields_rec, assumption)
-apply( fastsimp)
+apply( fastforce)
apply( tactic "safe_tac (put_claset HOL_cs @{context})")
apply( subst fields_rec)
apply( assumption)
@@ -410,8 +410,8 @@
apply( simp add: wf_cdecl_def)
apply( drule map_of_SomeD)
apply( subgoal_tac "md = Object")
-apply( fastsimp)
-apply( fastsimp)
+apply( fastforce)
+apply( fastforce)
apply( clarify)
apply( frule_tac C = C in method_rec)
apply( assumption)
@@ -445,8 +445,8 @@
apply( simp add: ws_cdecl_def)
apply( drule map_of_SomeD)
apply( subgoal_tac "md = Object")
-apply( fastsimp)
-apply( fastsimp)
+apply( fastforce)
+apply( fastforce)
apply( clarify)
apply( frule_tac C = C in method_rec)
apply( assumption)
@@ -648,7 +648,7 @@
apply( frule fields_rec, assumption)
apply( drule class_wf_struct, assumption)
apply( simp add: ws_cdecl_def wf_fdecl_def)
-apply( fastsimp)
+apply( fastforce)
apply( subst fields_rec)
apply( fast)
apply( assumption)