--- 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*)