src/HOL/Word/BinOperations.thy

   "!!b. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
   apply (induct n, clarsimp)
   apply (simp add: bin_rest_div zdiv_zmult2_eq)
   apply (case_tac b rule: bin_exhaust)
   apply simp
-  apply (simp add: Bit_def zmod_zmult_zmult1 p1mod22k
+  apply (simp add: Bit_def mod_mult_mult1 p1mod22k
               split: bit.split 
               cong: number_of_False_cong)
   done 
 
 subsection {* Miscellaneous lemmas *}