src/HOL/MicroJava/BV/BVNoTypeError.thy

   moreover {
     assume "\<not>(xcp \<noteq> None \<or> frs = [])"
     then obtain stk loc C sig pc frs' where
       xcp [simp]: "xcp = None" and
       frs [simp]: "frs = (stk,loc,C,sig,pc)#frs'" 
-      by (clarsimp simp add: neq_Nil_conv) fast
+      by (clarsimp simp add: neq_Nil_conv)
 
     from conforms obtain  ST LT rT maxs maxl ins et where
       hconf:  "G \<turnstile>h hp \<surd>" and
       "class":  "is_class G C" and
       meth:   "method (G, C) sig = Some (C, rT, maxs, maxl, ins, et)" and
       phi:    "Phi C sig ! pc = Some (ST,LT)" and
       frame:  "correct_frame G hp (ST,LT) maxl ins (stk,loc,C,sig,pc)" and
       frames: "correct_frames G hp Phi rT sig frs'"
-      by (auto simp add: correct_state_def) (rule that)
+      by (auto simp add: correct_state_def)
 
     from frame obtain
       stk: "approx_stk G hp stk ST" and
       loc: "approx_loc G hp loc LT" and
       pc:  "pc < length ins" and

       { assume "x \<noteq> Null"
         with x
         obtain D fs where
           hp: "hp (the_Addr x) = Some (D,fs)" and
           D:  "G \<turnstile> D \<preceq>C C"
-          by - (drule non_npD, assumption, clarsimp, blast)
+          by - (drule non_npD, assumption, clarsimp)
         hence "hp (the_Addr x) \<noteq> None" (is ?P1) by simp
         moreover
         from wf mth hp D
         have "method (G, cname_of hp x) (mn, ps) \<noteq> None" (is ?P2)
           by (auto dest: subcls_widen_methd)