src/Tools/Code/code_runtime.ML
changeset 62493 dd154240a53c
parent 62354 fdd6989cc8a0
child 62494 b90109b2487c
     1.1 --- a/src/Tools/Code/code_runtime.ML	Tue Mar 01 21:00:38 2016 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Mar 01 21:10:29 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 -    Secure.use_text ML_Env.local_context
     1.8 +    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 @@ -529,7 +529,7 @@
    1.13      allStruct    = #allStruct ML_Env.local_name_space,
    1.14      allSig       = #allSig ML_Env.local_name_space,
    1.15      allFunct     = #allFunct ML_Env.local_name_space},
    1.16 -  str_of_pos = #str_of_pos ML_Env.local_context,
    1.17 +  here = #here ML_Env.local_context,
    1.18    print = #print ML_Env.local_context,
    1.19    error = #error ML_Env.local_context};
    1.20  
    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 -      Secure.use_text notifying_context
    1.26 +      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 ());