diff -r 590a01e3efb4 -r c7cb1bf6efa0 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Jan 12 17:00:35 2024 +0100
+++ b/src/HOL/Code_Numeral.thy	Sat Jan 13 19:50:12 2024 +0000
@@ -348,7 +348,7 @@
   is take_bit .
 
 instance by (standard; transfer)
-  (fact bit_eq_rec bits_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
+  (fact bit_eq_rec bit_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
     bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
     exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
     even_mask_div_iff even_mult_exp_div_exp_iff
@@ -1107,7 +1107,7 @@
   is take_bit .
 
 instance by (standard; transfer)
-  (fact bit_eq_rec bits_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
+  (fact bit_eq_rec bit_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
     bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
     exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
     even_mask_div_iff even_mult_exp_div_exp_iff and_rec or_rec xor_rec