diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Library/Debug.thy --- a/src/HOL/Library/Debug.thy Thu Jan 02 08:37:52 2025 +0100 +++ b/src/HOL/Library/Debug.thy Thu Jan 02 08:37:55 2025 +0100 @@ -39,7 +39,6 @@ | constant Debug.flush \ (Eval) "Output.tracing/ (@{make'_string} _)" \ \note indirection via antiquotation\ | constant Debug.timing \ (Eval) "Timing.timeap'_msg" -code_reserved Eval Output Timing +code_reserved (Eval) Output Timing end -