src/HOL/Bali/WellType.thy

     case True
     with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases)
     then show ?thesis by blast
   next 
     case False then show ?thesis 
-      by (auto simp add: invmode_def split: split_if_asm)
+      by (auto simp add: invmode_def)
   qed
 qed
 
 lemma wt_Super: 
 "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk>