diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Library/Code_Real_Approx_By_Float.thy --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Thu Jan 02 08:37:52 2025 +0100 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Thu Jan 02 08:37:55 2025 +0100 @@ -82,7 +82,7 @@ arccos arctan]] -code_reserved SML Real +code_reserved (SML) Real code_printing type_constructor real \