src/Tools/Code/code_runtime.ML
changeset 62876 507c90523113
parent 62716 d80b9f4990e4
child 62889 99c7f31615c2
     1.1 --- a/src/Tools/Code/code_runtime.ML	Tue Apr 05 19:41:58 2016 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Apr 05 20:03:24 2016 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4    let
     1.5      val code = (prelude
     1.6        ^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
     1.7 -      ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
     1.8 +      ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))");
     1.9      val ctxt' = ctxt
    1.10        |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    1.11        |> Context.proof_map (exec ctxt false code);
    1.12 @@ -539,7 +539,7 @@
    1.13        ML_Compiler0.use_text notifying_context
    1.14          {line = 0, file = Path.implode filepath, verbose = false, debug = false}
    1.15          (File.read filepath);
    1.16 -    val thy'' = Context.the_theory (Context.the_thread_data ());
    1.17 +    val thy'' = Context.the_global_context ();
    1.18      val names = Loaded_Values.get thy'';
    1.19    in (names, thy'') end;
    1.20