src/HOL/Library/Debug.thy
changeset 81706 7beb0cf38292
parent 61585 a9599d3d7610
--- 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 \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" \<comment> \<open>note indirection via antiquotation\<close>
 | constant Debug.timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
 
-code_reserved Eval Output Timing
+code_reserved (Eval) Output Timing
 
 end
-