src/HOL/MicroJava/DFA/LBVComplete.thy

     with merge obtain
       app: "\<forall>(pc',s')\<in>set ss1. pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc'" 
            (is "?app ss1") and
       sum: "(map snd [(p',t') \<leftarrow> ss1 . p' = pc+1] ++_f x) = ?s1" 
            (is "?map ss1 ++_f x = _" is "?sum ss1 = _")
-      by (simp split: split_if_asm)
+      by (simp split: if_split_asm)
     from app less 
     have "?app ss2" by (blast dest: trans_r lesub_step_typeD)
     moreover {
       from ss1 have map1: "set (?map ss1) \<subseteq> A" by auto
       with x have "?sum ss1 \<in> A" by (auto intro!: plusplus_closed semilat)

 next
   case False
   have "?s1' = \<top> \<Longrightarrow> ?thesis" by simp
   moreover {
     assume "?s1' \<noteq> \<top>" 
-    with False have c: "s1 <=_r c!pc" by (simp add: wtc split: split_if_asm)
+    with False have c: "s1 <=_r c!pc" by (simp add: wtc split: if_split_asm)
     with less have "s2 <=_r c!pc" ..
     with False c have ?thesis by (simp add: wtc)
   }
   ultimately show ?thesis by (cases "?s1' = \<top>") auto
 qed

 next
   case False
   from suc_pc have pc: "pc < length \<phi>" by simp
   with stable have "?wtc \<noteq> \<top>" by (rule stable_wtc)
   with False have "?wtc = wti c pc (c!pc)" 
-    by (unfold wtc) (simp split: split_if_asm)
+    by (unfold wtc) (simp split: if_split_asm)
   also from pc False have "c!pc = \<phi>!pc" .. 
   finally have "?wtc = wti c pc (\<phi>!pc)" .
   also from stable suc_pc have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less)
   finally show ?thesis .
 qed