--- a/src/HOL/ex/Tarski.thy Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/ex/Tarski.thy Tue Feb 23 16:25:08 2016 +0100
@@ -659,7 +659,7 @@
apply (erule exE)
\<comment> \<open>define the lub for the interval as\<close>
apply (rule_tac x = "if S = {} then a else L" in exI)
-apply (simp (no_asm_simp) add: isLub_def split del: split_if)
+apply (simp (no_asm_simp) add: isLub_def split del: if_split)
apply (intro impI conjI)
\<comment> \<open>\<open>(if S = {} then a else L) \<in> interval r a b\<close>\<close>
apply (simp add: CL_imp_PO L_in_interval)