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 \Tools/code_evaluation.ML\ -code_reserved Eval Code_Evaluation +code_reserved + (Eval) Code_Evaluation ML_file \~~/src/HOL/Tools/value_command.ML\ @@ -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 \Generic reification\