diff -r 7891843d79bb -r a620a8756b7c src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Transcendental.thy	Tue Feb 23 18:04:31 2016 +0100
@@ -4265,11 +4265,11 @@
 
 lemma cos_tan: "\<bar>x\<bar> < pi/2 \<Longrightarrow> cos(x) = 1 / sqrt(1 + tan(x) ^ 2)"
   using cos_gt_zero_pi [of x]
-  by (simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
+  by (simp add: divide_simps tan_def real_sqrt_divide abs_if split: if_split_asm)
 
 lemma sin_tan: "\<bar>x\<bar> < pi/2 \<Longrightarrow> sin(x) = tan(x) / sqrt(1 + tan(x) ^ 2)"
   using cos_gt_zero [of "x"] cos_gt_zero [of "-x"]
-  by (force simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
+  by (force simp add: divide_simps tan_def real_sqrt_divide abs_if split: if_split_asm)
 
 lemma tan_mono_le: "-(pi/2) < x ==> x \<le> y ==> y < pi/2 \<Longrightarrow> tan(x) \<le> tan(y)"
   using less_eq_real_def tan_monotone by auto
@@ -4284,7 +4284,7 @@
 
 lemma tan_bound_pi2: "\<bar>x\<bar> < pi/4 \<Longrightarrow> \<bar>tan x\<bar> < 1"
   using tan_45 tan_monotone [of x "pi/4"] tan_monotone [of "-x" "pi/4"]
-  by (auto simp: abs_if split: split_if_asm)
+  by (auto simp: abs_if split: if_split_asm)
 
 lemma tan_cot: "tan(pi/2 - x) = inverse(tan x)"
   by (simp add: tan_def sin_diff cos_diff)