--- a/src/HOL/Library/Countable_Set.thy Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Library/Countable_Set.thy Tue Feb 23 16:25:08 2016 +0100
@@ -94,7 +94,7 @@
unfolding from_nat_into_def[abs_def]
using to_nat_on_finite[of S]
apply (subst bij_betw_cong)
- apply (split split_if)
+ apply (split if_split)
apply (simp add: bij_betw_def)
apply (auto cong: bij_betw_cong
intro: bij_betw_inv_into to_nat_on_finite)
@@ -303,7 +303,7 @@
assumes "countable X" obtains F where "\<And>i. F i \<subseteq> X" "\<And>i. F i \<subseteq> F (Suc i)" "\<And>i. finite (F i)" "(\<Union>i. F i) = X"
proof - show thesis
apply (rule that[of "\<lambda>i. if X = {} then {} else from_nat_into X ` {..i}"])
- apply (auto simp: image_iff Ball_def intro: from_nat_into split: split_if_asm)
+ apply (auto simp: image_iff Ball_def intro: from_nat_into split: if_split_asm)
proof -
fix x n assume "x \<in> X" "\<forall>i m. m \<le> i \<longrightarrow> x \<noteq> from_nat_into X m"
with from_nat_into_surj[OF \<open>countable X\<close> \<open>x \<in> X\<close>]