src/HOL/Statespace/DistinctTreeProver.thy

       with Node.hyps
       have "set_of r' \<subseteq> set_of r"
         by simp
       with l'_l Some x_l_Some del
       show ?thesis
-        by (auto split: split_if_asm)
+        by (auto split: if_split_asm)
     next
       case None
       with l'_l Some x_l_Some del
       show ?thesis
-        by (fastforce split: split_if_asm)
+        by (fastforce split: if_split_asm)
     qed
   next
     case None
     note x_l_None = this
     show ?thesis

       with Node.hyps
       have "set_of r' \<subseteq> set_of r"
         by simp
       with Some x_l_None del
       show ?thesis
-        by (fastforce split: split_if_asm)
+        by (fastforce split: if_split_asm)
     next
       case None
       with x_l_None del
       show ?thesis
-        by (fastforce split: split_if_asm)
+        by (fastforce split: if_split_asm)
     qed
   qed
 qed
 
 lemma delete_Some_all_distinct:

         by fastforce
     next
       case None
       with x_l_None del dist_l dist_r d dist_l_r
       show ?thesis
-        by (fastforce split: split_if_asm)
+        by (fastforce split: if_split_asm)
     qed
   qed
 qed
 
 lemma delete_None_set_of_conv: "delete x t = None = (x \<notin> set_of t)"

       from Node.hyps (2) [OF Some]
       obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'"
         by simp
       from x_r x_l Some x_l_Some del 
       show ?thesis
-        by (clarsimp split: split_if_asm)
+        by (clarsimp split: if_split_asm)
     next
       case None
       then have "x \<notin> set_of r"
         by (simp add: delete_None_set_of_conv)
       with x_l None x_l_Some del
       show ?thesis
-        by (clarsimp split: split_if_asm)
+        by (clarsimp split: if_split_asm)
     qed
   next
     case None
     note x_l_None = this
     then have x_notin_l: "x \<notin> set_of l"

       from Node.hyps (2) [OF Some]
       obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'"
         by simp
       from x_r x_notin_l Some x_l_None del 
       show ?thesis
-        by (clarsimp split: split_if_asm)
+        by (clarsimp split: if_split_asm)
     next
       case None
       then have "x \<notin> set_of r"
         by (simp add: delete_None_set_of_conv)
       with None x_l_None x_notin_l del
       show ?thesis
-        by (clarsimp split: split_if_asm)
+        by (clarsimp split: if_split_asm)
     qed
   qed
 qed