diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Thu Jan 02 08:37:52 2025 +0100 +++ b/src/HOL/Code_Numeral.thy Thu Jan 02 08:37:55 2025 +0100 @@ -780,7 +780,8 @@ subsection \Serializer setup for target language integers\ -code_reserved Eval int Integer abs +code_reserved + (Eval) int Integer abs code_printing type_constructor integer \