src/Tools/Code/code_thingol.ML

   val group_stmts: Proof.context -> program
     -> ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list
       * ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list
 
   val read_const_exprs: Proof.context -> string list -> string list
-  val consts_program: theory -> string list -> program
+  val consts_program: Proof.context -> string list -> program
   val dynamic_conv: Proof.context -> (program
     -> typscheme * iterm -> Code_Symbol.T list -> conv)
     -> conv
   val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program
     -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)

 (
   type T = program;
   val empty = Code_Symbol.Graph.empty;
 );
 
-fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing =
-  Program.change_yield (if ignore_cache then NONE else SOME thy)
+fun invoke_generation ignore_cache ctxt (algebra, eqngr) generate thing =
+  Program.change_yield
+    (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
     (fn program => ([], program)
-      |> generate (Proof_Context.init_global thy) algebra eqngr thing
+      |> generate ctxt algebra eqngr thing
       |-> (fn thing => fn (_, program) => (thing, program)));
 
 
 (* program generation *)
 
-fun consts_program_internal thy permissive consts =
+fun consts_program_internal ctxt permissive consts =
   let
     fun generate_consts ctxt algebra eqngr =
       fold_map (ensure_const ctxt algebra eqngr permissive);
   in
-    invoke_generation permissive thy
-      (Code_Preproc.obtain false (Proof_Context.init_global thy) consts [])
+    invoke_generation permissive ctxt
+      (Code_Preproc.obtain false ctxt consts [])
       generate_consts consts
     |> snd
   end;
 
 fun consts_program_permissive thy = consts_program_internal thy true;

   end;
 
 fun dynamic_evaluation eval ctxt algebra eqngr t =
   let
     val ((program, (vs_ty_t', deps)), _) =
-      invoke_generation false (Proof_Context.theory_of ctxt)
+      invoke_generation false ctxt
         (algebra, eqngr) ensure_value t;
   in eval program t vs_ty_t' deps end;
 
 fun dynamic_conv ctxt conv =
   Code_Preproc.dynamic_conv ctxt

 fun static_evaluation ctxt consts algebra eqngr static_eval =
   let
     fun generate_consts ctxt algebra eqngr =
       fold_map (ensure_const ctxt algebra eqngr false);
     val (deps, program) =
-      invoke_generation true (Proof_Context.theory_of ctxt)
+      invoke_generation true ctxt
         (algebra, eqngr) generate_consts consts;
   in static_eval { program = program, deps = deps } end;
 
 fun static_evaluation_thingol ctxt consts algebra eqngr static_eval =
   let

 
 fun read_const_exprs_all ctxt = op @ o read_const_exprs_internal ctxt;
 
 fun read_const_exprs ctxt const_exprs =
   let
-    val (consts, consts_permissive) = read_const_exprs_internal ctxt const_exprs;
+    val (consts, consts_permissive) =
+      read_const_exprs_internal ctxt const_exprs;
     val consts' = implemented_deps
-      (consts_program_permissive (Proof_Context.theory_of ctxt) consts_permissive);
+      (consts_program_permissive ctxt consts_permissive);
   in union (op =) consts' consts end;
 
 
 (** diagnostic commands **)