1.1 --- a/src/HOL/Word/Word.thy	Tue Feb 23 15:37:18 2016 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Tue Feb 23 16:25:08 2016 +0100
     1.3 @@ -1545,7 +1545,7 @@
     1.4  fun uint_arith_simpset ctxt = 
     1.5    ctxt addsimps @{thms uint_arith_simps}
     1.6       delsimps @{thms word_uint.Rep_inject}
     1.7 -     |> fold Splitter.add_split @{thms split_if_asm}
     1.8 +     |> fold Splitter.add_split @{thms if_split_asm}
     1.9       |> fold Simplifier.add_cong @{thms power_False_cong}
    1.10  
    1.11  fun uint_arith_tacs ctxt = 
    1.12 @@ -1748,7 +1748,7 @@
    1.13    using [[simproc del: linordered_ring_less_cancel_factor]]
    1.14    apply (unfold udvd_def)
    1.15    apply clarify
    1.16 -  apply (simp add: uint_arith_simps split: split_if_asm)
    1.17 +  apply (simp add: uint_arith_simps split: if_split_asm)
    1.18     prefer 2 
    1.19     apply (insert uint_range' [of s])[1]
    1.20     apply arith
    1.21 @@ -2047,7 +2047,7 @@
    1.22  fun unat_arith_simpset ctxt = 
    1.23    ctxt addsimps @{thms unat_arith_simps}
    1.24       delsimps @{thms word_unat.Rep_inject}
    1.25 -     |> fold Splitter.add_split @{thms split_if_asm}
    1.26 +     |> fold Splitter.add_split @{thms if_split_asm}
    1.27       |> fold Simplifier.add_cong @{thms power_False_cong}
    1.28  
    1.29  fun unat_arith_tacs ctxt =   
    1.30 @@ -4217,7 +4217,7 @@
    1.31  
    1.32    show ?thesis
    1.33    apply (unfold word_rot_defs)
    1.34 -  apply (simp only: split: split_if)
    1.35 +  apply (simp only: split: if_split)
    1.36    apply (safe intro!: abl_cong)
    1.37    apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse'] 
    1.38                      to_bl_rotl