diff -r 29800666e526 -r 842917225d56 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Library/RBT_Impl.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -155,7 +155,7 @@
 next
   case (Branch color t1 a b t2)
   let ?A = "Set.insert a (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2))"
-  have "dom (rbt_lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm)
+  have "dom (rbt_lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: if_split_asm)
   moreover from Branch have "finite (insert a (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2)))" by simp
   ultimately show ?case by (rule finite_subset)
 qed