src/Tools/Code/code_runtime.ML
changeset 62889 99c7f31615c2
parent 62876 507c90523113
child 62902 3c0f53eae166
     1.1 --- a/src/Tools/Code/code_runtime.ML	Wed Apr 06 14:08:57 2016 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Wed Apr 06 16:33:33 2016 +0200
     1.3 @@ -86,9 +86,9 @@
     1.4  
     1.5  fun value ctxt (get, put, put_ml) (prelude, value) =
     1.6    let
     1.7 -    val code = (prelude
     1.8 -      ^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
     1.9 -      ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))");
    1.10 +    val code =
    1.11 +      prelude ^ "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^
    1.12 +      put_ml ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))";
    1.13      val ctxt' = ctxt
    1.14        |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    1.15        |> Context.proof_map (exec ctxt false code);
    1.16 @@ -534,7 +534,7 @@
    1.17  fun use_file filepath thy =
    1.18    let
    1.19      val thy' = Loaded_Values.put [] thy;
    1.20 -    val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
    1.21 +    val _ = Context.put_generic_context ((SOME o Context.Theory) thy');
    1.22      val _ =
    1.23        ML_Compiler0.use_text notifying_context
    1.24          {line = 0, file = Path.implode filepath, verbose = false, debug = false}