diff -r 29800666e526 -r 842917225d56 src/HOL/HOLCF/IOA/TLS.thy
--- a/src/HOL/HOLCF/IOA/TLS.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/HOLCF/IOA/TLS.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -140,7 +140,7 @@
               \<^bold>\<longrightarrow> (Next (Init (\<lambda>(s, a, t). Q s))))"
   apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
   apply clarify
-  apply (simp split add: split_if)
+  apply (simp split add: if_split)
   text \<open>\<open>TL = UU\<close>\<close>
   apply (rule conjI)
   apply (pair ex)