src/Tools/Code/code_runtime.ML

   #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]);
        (*avoid further pervasive infix names*)
 
 val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false);
 
-fun exec ctxt verbose code =
- (if Config.get ctxt trace then tracing code else ();
-  ML_Context.exec (fn () =>
-    ML_Compiler0.ML ML_Env.context
-      {line = 0, file = "generated code", verbose = verbose, debug = false} code));
+fun compile_ML verbose code context =
+ (if Config.get_generic context trace then tracing code else ();
+  ML_Context.exec (fn () => ML_Compiler0.ML ML_Env.context
+    {line = 0, file = "generated code", verbose = verbose,
+       debug = false} code) context);
 
 fun value ctxt (get, put, put_ml) (prelude, value) =
   let
     val code =
       prelude ^ "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^
       put_ml ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))";
     val ctxt' = ctxt
       |> put (fn () => error ("Bad computation for " ^ quote put_ml))
-      |> Context.proof_map (exec ctxt false code);
+      |> Context.proof_map (compile_ML false code);
   in get ctxt' () end;
 
 
 (* computation as evaluation into ML language values *)
 

   (const, [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')))]));
 
 fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy =
       thy
       |> Code_Target.add_reserved target module_name
-      |> Context.theory_map (exec (Proof_Context.init_global thy (*FIXME*)) true code)
+      |> Context.theory_map (compile_ML true code)
       |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
       |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
       |> fold (add_eval_const o apsnd Code_Printer.str) const_map
   | process_reflection (code, _) _ (SOME file_name) thy =
       let