
diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Code_Evaluation.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -88,7 +88,8 @@
 
 ML_file \<open>Tools/code_evaluation.ML\<close>
 
-code_reserved Eval Code_Evaluation
+code_reserved
+  (Eval) Code_Evaluation
 
 ML_file \<open>~~/src/HOL/Tools/value_command.ML\<close>
 
@@ -128,7 +129,8 @@
        (term_of (- i)))"
   by (rule term_of_anything [THEN meta_eq_to_obj_eq])
 
-code_reserved Eval HOLogic
+code_reserved
+  (Eval) HOLogic
 
 
 subsection \<open>Generic reification\<close>




