diff -r 29800666e526 -r 842917225d56 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Map.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -358,10 +358,10 @@
 by (simp add: restrict_map_def)
 
 lemma ran_restrictD: "y \<in> ran (m|`A) \<Longrightarrow> \<exists>x\<in>A. m x = Some y"
-by (auto simp: restrict_map_def ran_def split: split_if_asm)
+by (auto simp: restrict_map_def ran_def split: if_split_asm)
 
 lemma dom_restrict [simp]: "dom (m|`A) = dom m \<inter> A"
-by (auto simp: restrict_map_def dom_def split: split_if_asm)
+by (auto simp: restrict_map_def dom_def split: if_split_asm)
 
 lemma restrict_upd_same [simp]: "m(x\<mapsto>y)|`(-{x}) = m|`(-{x})"
 by (rule ext) (auto simp: restrict_map_def)
@@ -429,7 +429,7 @@
 apply (induct xs arbitrary: x y ys f)
  apply simp
 apply (case_tac ys)
- apply (auto split: split_if simp: fun_upd_twist)
+ apply (auto split: if_split simp: fun_upd_twist)
 done
 
 lemma map_upds_twist [simp]:
@@ -691,7 +691,7 @@
 lemma dom_eq_singleton_conv: "dom f = {x} \<longleftrightarrow> (\<exists>v. f = [x \<mapsto> v])"
 proof(rule iffI)
   assume "\<exists>v. f = [x \<mapsto> v]"
-  thus "dom f = {x}" by(auto split: split_if_asm)
+  thus "dom f = {x}" by(auto split: if_split_asm)
 next
   assume "dom f = {x}"
   then obtain v where "f x = Some v" by auto