src/HOL/Library/Char_nat.thy

       mult_assoc [symmetric] div_mult_self_is_m [OF 16] by simp
   have aux4: "(k * 256 + l) mod 16 = l mod 16"
     unfolding 256 mult_assoc [symmetric] mod_mult_self3 ..
   show ?thesis
     by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair
-      nat_of_nibble_of_nat mod_mult_distrib
+      nat_of_nibble_of_nat mult_mod_left
       n aux3 l_256 aux4 mod_add_eq [of "256 * k"] l_div_256)
 qed
 
 lemma nibble_pair_of_nat_char:
   "nibble_pair_of_nat (nat_of_char (Char n m)) = (n, m)"