1.1 --- a/src/Tools/Code/code_runtime.ML	Tue Mar 01 21:10:29 2016 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Mar 01 22:11:36 2016 +0100
     1.3 @@ -82,7 +82,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 -    use_text ML_Env.local_context
     1.8 +    ML_Compiler0.use_text ML_Env.local_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 @@ -509,7 +509,7 @@
    1.13  
    1.14  fun abort _ = error "Only value bindings allowed.";
    1.15  
    1.16 -val notifying_context : use_context =
    1.17 +val notifying_context : ML_Compiler0.context =
    1.18   {name_space =
    1.19     {lookupVal    = #lookupVal ML_Env.local_name_space,
    1.20      lookupType   = #lookupType ML_Env.local_name_space,
    1.21 @@ -540,7 +540,7 @@
    1.22      val thy' = Loaded_Values.put [] thy;
    1.23      val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
    1.24      val _ =
    1.25 -      use_text notifying_context
    1.26 +      ML_Compiler0.use_text notifying_context
    1.27          {line = 0, file = Path.implode filepath, verbose = false, debug = false}
    1.28          (File.read filepath);
    1.29      val thy'' = Context.the_theory (Context.the_thread_data ());