src/HOL/Bali/Conform.thy

 \<rbrakk> \<Longrightarrow>  G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r"
 apply (auto simp add: oconf_def)
 apply (drule_tac var_tys_Some_eq [THEN iffD1]) 
 defer
 apply (subst obj_ty_cong)
-apply(auto dest!: fields_table_SomeD obj_ty_CInst1 obj_ty_Arr1
-           split add: sum.split_asm obj_tag.split_asm)
+apply (auto dest!: fields_table_SomeD split add: sum.split_asm obj_tag.split_asm)
 done
 
 section "state conformance"
 
 definition

   "((raise_if c xn x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
 by (auto simp: abrupt_if_def)
 
 lemma conforms_error_if [iff]: 
   "((error_if c err x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
-by (auto simp: abrupt_if_def split: split_if)
+by (auto simp: abrupt_if_def)
 
 lemma conforms_NormI: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> Norm s\<Colon>\<preceq>(G, L)"
 by (auto simp: conforms_def Let_def)
 
 lemma conforms_absorb [rule_format]: