src/HOL/Bali/TypeSafe.thy

                 statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
                          = {((statDeclT,statM),pTs')}" and
                  mode: "mode = invmode statM e" and
                     T: "T =Inl (resTy statM)" and
         eq_accC_accC': "accC=accC'"
-      by (rule wt_elim_cases) auto
+      by (rule wt_elim_cases) fastsimp+
     from conf_s0 wt_e hyp_e 
     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
            conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT" and
            error_free_s1: "error_free s1" 
       by force

       from eq_s3'_s3 False keep_abrupt eval_methd
       have "s4=s3'"
 	by auto
       ultimately have
 	"set_lvars (locals (store s2)) s4 = s2"
-	by (cases s2,cases s4) (simp add: init_lvars_def2)
+	by (cases s2) (cases s4, fastsimp simp add: init_lvars_def2)
       with False conf_s2 error_free_s2
       show ?thesis
 	by auto
     next
       case True

 	have "s4=s3'"
 	  by auto
 	ultimately have
 	  "set_lvars (locals (store s2)) s4 
            = (Some (Xcpt (Std NullPointer)),store s2)"
-	  by (cases s2,cases s4) (simp add: init_lvars_def2)
+	  by (cases s2) (cases s4, fastsimp simp add: init_lvars_def2)
 	with conf_s2 error_free_s2
 	show ?thesis
 	  by (cases s2) (auto dest: conforms_NormI)
       next
 	case True