src/HOL/MicroJava/Comp/CorrComp.thy

   & (length ps = length pTs') & (E\<turnstile>a::Class C)
   & (\<exists> pTs md rT. 
        E\<turnstile>ps[::]pTs & max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')})"
 apply (simp only: wtpd_expr_def wtpd_exprs_def)
 apply (erule exE)
-apply (ind_cases2 "E \<turnstile> {C}a..mn( {pTs'}ps) :: T" for T)
+apply (ind_cases "E \<turnstile> {C}a..mn( {pTs'}ps) :: T" for T)
 apply (auto simp: max_spec_preserves_length)
 done
 
 lemma wtpd_blk: 
   "\<lbrakk> method (G, D) (md, pTs) = Some (D, rT, (pns, lvars, blk, res)); 

   "(\<forall> Ts. (E \<turnstile> es [::] Ts) = list_all2 (\<lambda>e T. E \<turnstile> e :: T) es Ts)"
 apply (rule list.induct)
 apply simp
 apply (rule allI)
 apply (rule iffI)
-  apply (ind_cases2 "E \<turnstile> [] [::] Ts" for Ts, assumption)
+  apply (ind_cases "E \<turnstile> [] [::] Ts" for Ts, assumption)
   apply simp apply (rule WellType.Nil)
 apply (simp add: list_all2_Cons1)
 apply (rule allI)
 apply (rule iffI)
   apply (rename_tac a exs Ts)
-  apply (ind_cases2 "E \<turnstile> a # exs  [::] Ts" for a exs Ts) apply blast
+  apply (ind_cases "E \<turnstile> a # exs  [::] Ts" for a exs Ts) apply blast
   apply (auto intro: WellType.Cons)
 done
 
 
 lemma conf_bool: "G,h \<turnstile> v::\<preceq>PrimT Boolean \<Longrightarrow> \<exists> b. v = Bool b"