diff -r 29800666e526 -r 842917225d56 src/HOL/Statespace/DistinctTreeProver.thy
--- a/src/HOL/Statespace/DistinctTreeProver.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -134,12 +134,12 @@
         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
@@ -152,12 +152,12 @@
         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
@@ -221,7 +221,7 @@
       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
@@ -257,14 +257,14 @@
         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
@@ -279,14 +279,14 @@
         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