diff -r bd9a5e128c31 -r 04b1ce7efd22 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Tue Sep 28 22:45:52 2021 +0200
+++ b/src/Tools/Code/code_runtime.ML	Tue Sep 28 22:39:27 2021 +0200
@@ -653,7 +653,7 @@
 
 fun ml_computation_check_antiq raw_spec ctxt =
   let
-    val cTs = insert (op =) (dest_Const \<^const>\<open>holds\<close>) (prep_spec ctxt raw_spec);
+    val cTs = insert (op =) (dest_Const \<^Const>\<open>holds\<close>) (prep_spec ctxt raw_spec);
   in (print_computation_check ctxt, register_computation cTs \<^typ>\<open>prop\<close> ctxt) end;
 
 end; (*local*)