diff -r 707748d3d186 -r 714528f42922 src/HOL/Library/Code_Abstract_Char.thy
--- a/src/HOL/Library/Code_Abstract_Char.thy	Mon Jul 11 15:04:04 2022 +0200
+++ b/src/HOL/Library/Code_Abstract_Char.thy	Tue Jul 12 10:38:13 2022 +0000
@@ -17,7 +17,7 @@
   by (simp add: integer_of_char_def)
 
 lemma char_of_integer_code [code]:
-  \<open>integer_of_char (char_of_integer k) = (if 0 \<le> k \<and> k < 256 then k else take_bit 8 k)\<close>
+  \<open>integer_of_char (char_of_integer k) = (if 0 \<le> k \<and> k < 256 then k else k mod 256)\<close>
   by (simp add: integer_of_char_def char_of_integer_def take_bit_eq_mod unique_euclidean_semiring_numeral_class.mod_less)
 
 lemma of_char_code [code]:
@@ -49,7 +49,7 @@
 lemma Char_code [code]:
   \<open>integer_of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) = byte b0 b1 b2 b3 b4 b5 b6 b7\<close>
   by (simp add: integer_of_char_def)
-                     
+
 lemma digit_0_code [code]:
   \<open>digit0 c \<longleftrightarrow> bit (integer_of_char c) 0\<close>
   by (cases c) (simp add: integer_of_char_def)