diff -r 5ae24f33d343 -r a4b68bf18f8d src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Wed Feb 24 15:51:01 2016 +0000
+++ b/src/HOL/Deriv.thy	Wed Feb 24 16:00:57 2016 +0000
@@ -961,7 +961,7 @@
     fix h::real
     assume "0 < h" "h < s"
     with all [of h] show "f x < f (x+h)"
-    proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm)
+    proof (simp add: abs_if pos_less_divide_eq split add: if_split_asm)
       assume "~ (f (x+h) - f x) / h < l" and h: "0 < h"
       with l
       have "0 < (f (x+h) - f x) / h" by arith
@@ -990,7 +990,7 @@
     fix h::real
     assume "0 < h" "h < s"
     with all [of "-h"] show "f x < f (x-h)"
-    proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm)
+    proof (simp add: abs_if pos_less_divide_eq split add: if_split_asm)
       assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
       with l
       have "0 < (f (x-h) - f x) / h" by arith