--- a/src/HOL/Metis_Examples/Tarski.thy Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy Tue Feb 23 16:25:08 2016 +0100
@@ -711,7 +711,7 @@
apply (erule exE)
-- {* define the lub for the interval as *}
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)
-- {* @{text "(if S = {} then a else L) \<in> interval r a b"} *}
apply (simp add: CL_imp_PO L_in_interval)