src/HOL/Word/WordBitwise.thy

    {lhss = map (fn t => t $ @{term "n :: nat"}) ts,
     proc = K (nat_get_Suc_simproc_fn n_sucs), identifier = []};
 
 val no_split_ss =
   simpset_of (put_simpset HOL_ss @{context}
-    |> Splitter.del_split @{thm split_if});
+    |> Splitter.del_split @{thm if_split});
 
 val expand_word_eq_sss =
   (simpset_of (put_simpset HOL_basic_ss @{context} addsimps
        @{thms word_eq_rbl_eq word_le_rbl word_less_rbl word_sle_rbl word_sless_rbl}),
   map simpset_of [