src/HOL/MicroJava/Comp/CorrCompTp.thy

               (OK (Some (start_ST, start_LT C pTs mxl)))"
 apply (simp add: check_type_def wf_mhead_def start_ST_def start_LT_def)
 apply (simp add: check_type_simps)
 apply (simp only: list_def)
 apply (auto simp: err_def)
-apply (subgoal_tac "set (replicate mxl Err) \<subseteq>  {Err}")
-apply blast
-apply (rule subset_replicate)
 done
 
 
 lemma wt_method_comp_aux: "\<lbrakk>   bc' = bc @ [Return]; f' = (f \<box> nochangeST);
   bc_mt_corresp bc f sttp0 cG rT (1+length pTs+mxl) (length bc);