diff -r 29800666e526 -r 842917225d56 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Divides.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -1002,7 +1002,7 @@
   assume "m \<noteq> 0"
   hence "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
     unfolding divmod_nat_rel_def
-    by (auto split: split_if_asm, simp_all add: algebra_simps)
+    by (auto split: if_split_asm, simp_all add: algebra_simps)
   moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
   ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
   thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)
@@ -1660,7 +1660,7 @@
 
 lemma unique_quotient:
   "divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> q = q'"
-apply (simp add: divmod_int_rel_def linorder_neq_iff split: split_if_asm)
+apply (simp add: divmod_int_rel_def linorder_neq_iff split: if_split_asm)
 apply (blast intro: order_antisym
              dest: order_eq_refl [THEN unique_quotient_lemma]
              order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
@@ -2072,7 +2072,7 @@
       ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
 by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
                    zero_less_mult_iff distrib_left [symmetric]
-                   zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
+                   zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
 
 lemma zdiv_zmult2_eq:
   fixes a b c :: int