src/Tools/Code/code_runtime.ML
changeset 69597 ff784d5a5bfb
parent 69593 3dda49e08b9d
child 69623 ef02c5e051e5
     1.1 --- a/src/Tools/Code/code_runtime.ML	Sat Jan 05 17:00:43 2019 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Sat Jan 05 17:24:33 2019 +0100
     1.3 @@ -651,7 +651,7 @@
     1.4  
     1.5  fun ml_computation_check_antiq raw_spec ctxt =
     1.6    let
     1.7 -    val cTs = insert (op =) (dest_Const @{const holds}) (prep_spec ctxt raw_spec);
     1.8 +    val cTs = insert (op =) (dest_Const \<^const>\<open>holds\<close>) (prep_spec ctxt raw_spec);
     1.9    in (print_computation_check ctxt, register_computation cTs \<^typ>\<open>prop\<close> ctxt) end;
    1.10  
    1.11  end; (*local*)