src/HOL/Bali/Evaln.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
     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1"
       by blast
     with wf conf_s0 wt_e
     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and

                 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
     obtain n1 where
       evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
       by (rules dest: hyp_e)
     from wf eval_e conf_s0 wt_e

                 wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
             accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
                 stat: "stat=is_static f" and
                accC': "accC'=accC" and
 	           T: "T=(Inl (type f))"
-       by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
+       by (rule wt_elim_cases) (fastsimp simp add: member_is_static_simp)
     from wf wt_e 
     have iscls_statC: "is_class G statC"
       by (auto dest: ty_expr_is_type type_is_class)
     with wf accfield 
     have iscls_statDeclC: "is_class G statDeclC"