src/Tools/Code/code_runtime.ML
changeset 62902 3c0f53eae166
parent 62889 99c7f31615c2
child 63064 2f18172214c8
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu Apr 07 15:32:47 2016 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Apr 07 16:53:43 2016 +0200
     1.3 @@ -81,7 +81,7 @@
     1.4  fun exec ctxt verbose code =
     1.5   (if Config.get ctxt trace then tracing code else ();
     1.6    ML_Context.exec (fn () =>
     1.7 -    ML_Compiler0.use_text ML_Env.context
     1.8 +    ML_Compiler0.ML ML_Env.context
     1.9        {line = 0, file = "generated code", verbose = verbose, debug = false} code));
    1.10  
    1.11  fun value ctxt (get, put, put_ml) (prelude, value) =
    1.12 @@ -536,7 +536,7 @@
    1.13      val thy' = Loaded_Values.put [] thy;
    1.14      val _ = Context.put_generic_context ((SOME o Context.Theory) thy');
    1.15      val _ =
    1.16 -      ML_Compiler0.use_text notifying_context
    1.17 +      ML_Compiler0.ML notifying_context
    1.18          {line = 0, file = Path.implode filepath, verbose = false, debug = false}
    1.19          (File.read filepath);
    1.20      val thy'' = Context.the_global_context ();