prefer proof context over background theory
authorhaftmann
Wed, 26 Feb 2014 11:57:52 +0100 (2014-02-26)
changeset 55757 9fc71814b8c1
parent 55756 565a20b22f09
child 55758 385f7573f8f5
prefer proof context over background theory
NEWS
src/Doc/Codegen/Further.thy
src/HOL/HOL.thy
src/HOL/Library/Code_Abstract_Nat.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/code_evaluation.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_simp.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
--- a/NEWS	Wed Feb 26 10:10:38 2014 +0100
+++ b/NEWS	Wed Feb 26 11:57:52 2014 +0100
@@ -91,9 +91,14 @@
 
 *** HOL ***
 
+* Code generator: explicit proof contexts in many ML interfaces.
+INCOMPATIBILITY.
+
 * Code generator: minimize exported identifiers by default.
+Minor INCOMPATIBILITY.
 
 * Code generation for SML and OCaml: dropped arcane "no_signatures" option.
+Minor INCOMPATIBILITY.
 
 * Simproc "finite_Collect" is no longer enabled by default, due to
 spurious crashes and other surprises.  Potential INCOMPATIBILITY.
--- a/src/Doc/Codegen/Further.thy	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/Doc/Codegen/Further.thy	Wed Feb 26 11:57:52 2014 +0100
@@ -258,7 +258,7 @@
   @{index_ML Code_Preproc.map_pre: "(Proof.context -> Proof.context) -> theory -> theory"} \\
   @{index_ML Code_Preproc.map_post: "(Proof.context -> Proof.context) -> theory -> theory"} \\
   @{index_ML Code_Preproc.add_functrans: "
-    string * (theory -> (thm * bool) list -> (thm * bool) list option)
+    string * (Proof.context -> (thm * bool) list -> (thm * bool) list option)
       -> theory -> theory"} \\
   @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
   @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
--- a/src/HOL/HOL.thy	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/HOL.thy	Wed Feb 26 11:57:52 2014 +0100
@@ -1903,20 +1903,21 @@
 
 subsubsection {* Evaluation and normalization by evaluation *}
 
-ML {*
-fun eval_tac ctxt =
-  let val conv = Code_Runtime.dynamic_holds_conv (Proof_Context.theory_of ctxt)
-  in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
-*}
-
-method_setup eval = {* Scan.succeed (SIMPLE_METHOD' o eval_tac) *}
-  "solve goal by evaluation"
+method_setup eval = {*
+let
+  fun eval_tac ctxt =
+    let val conv = Code_Runtime.dynamic_holds_conv ctxt
+    in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
+in
+  Scan.succeed (SIMPLE_METHOD' o eval_tac)
+end
+*} "solve goal by evaluation"
 
 method_setup normalization = {*
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD'
       (CHANGED_PROP o
-        (CONVERSION (Nbe.dynamic_conv (Proof_Context.theory_of ctxt))
+        (CONVERSION (Nbe.dynamic_conv ctxt)
           THEN_ALL_NEW (TRY o rtac TrueI))))
 *} "solve goal by normalization"
 
--- a/src/HOL/Library/Code_Abstract_Nat.thy	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy	Wed Feb 26 11:57:52 2014 +0100
@@ -50,8 +50,9 @@
 setup {*
 let
 
-fun remove_suc thy thms =
+fun remove_suc ctxt thms =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val vname = singleton (Name.variant_list (map fst
       (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
     val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 26 11:57:52 2014 +0100
@@ -1914,7 +1914,7 @@
           in
             rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
               (Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
-                thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> Limited_Sequence.map proc)
+                ctxt NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> Limited_Sequence.map proc)
                   t' [] nrandom size
                 |> Random_Engine.run)
               depth true)) ())
@@ -1922,14 +1922,14 @@
       | DSeq =>
           rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
             (Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
-              thy NONE Limited_Sequence.map t' []) (Code_Numeral.natural_of_integer (the_single arguments)) true)) ())
+              ctxt NONE Limited_Sequence.map t' []) (Code_Numeral.natural_of_integer (the_single arguments)) true)) ())
       | Pos_Generator_DSeq =>
           let
             val depth = Code_Numeral.natural_of_integer (the_single arguments)
           in
             rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
               (Code_Runtime.dynamic_value_strict (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Core.put_new_dseq_result")
-              thy NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.map proc)
+              ctxt NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.map proc)
               t' [] depth))) ())
           end
       | New_Pos_Random_DSeq =>
@@ -1943,7 +1943,7 @@
               (fn () => fst (Lazy_Sequence.yieldn k
                 (Code_Runtime.dynamic_value_strict
                   (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
-                  thy NONE
+                  ctxt NONE
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
                     |> Lazy_Sequence.map (apfst proc))
                     t' [] nrandom size seed depth))) ()))
@@ -1951,7 +1951,7 @@
               (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
                 (Code_Runtime.dynamic_value_strict
                   (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
-                  thy NONE
+                  ctxt NONE
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
                     |> Lazy_Sequence.map proc)
                     t' [] nrandom size seed depth))) ())
@@ -1959,7 +1959,7 @@
       | _ =>
           rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Predicate.yieldn k
             (Code_Runtime.dynamic_value_strict (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
-              thy NONE Predicate.map t' []))) ()))
+              ctxt NONE Predicate.map t' []))) ()))
      handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
   in ((T, ts), statistics) end;
 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Feb 26 11:57:52 2014 +0100
@@ -296,7 +296,7 @@
           let
             val compiled_term =
               Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
-                thy4 (SOME target)
+                (Proof_Context.init_global thy4) (SOME target)
                 (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (Limited_Sequence.map o map) proc)
                 qc_term []
           in
@@ -309,7 +309,7 @@
             val compiled_term =
               Code_Runtime.dynamic_value_strict
                 (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
-                thy4 (SOME target)
+                (Proof_Context.init_global thy4) (SOME target)
                 (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
                   g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
                   qc_term []
@@ -325,7 +325,7 @@
             val compiled_term =
               Code_Runtime.dynamic_value_strict
                 (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Quickcheck.put_new_dseq_result")
-                thy4 (SOME target)
+                (Proof_Context.init_global thy4) (SOME target)
                 (fn proc => fn g => fn depth => g depth |> (Lazy_Sequence.map o map) proc)
                 qc_term []
           in
@@ -336,7 +336,7 @@
             val compiled_term =
               Code_Runtime.dynamic_value_strict
                 (CPS_Result.get, put_cps_result, "Predicate_Compile_Quickcheck.put_cps_result")
-                thy4 (SOME target)
+                (Proof_Context.init_global thy4) (SOME target)
                 (fn proc => fn g => fn depth => g depth |> Option.map (apsnd (map proc)))
                 qc_term []
           in
@@ -346,7 +346,7 @@
           let
             val compiled_term = Code_Runtime.dynamic_value_strict
               (Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
-                thy4 (SOME target) (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
+                (Proof_Context.init_global thy4) (SOME target) (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
                   g depth nrandom size seed |> (Predicate.map o map) proc)
                 qc_term []
           in
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Feb 26 11:57:52 2014 +0100
@@ -471,7 +471,6 @@
 
 fun compile_generator_expr_raw ctxt ts =
   let
-    val thy = Proof_Context.theory_of ctxt
     val mk_generator_expr = 
       if Config.get ctxt fast then mk_fast_generator_expr
       else if Config.get ctxt bounded_forall then mk_bounded_forall_generator_expr
@@ -479,7 +478,7 @@
     val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts;
     val compile = Code_Runtime.dynamic_value_strict
       (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
-      thy (SOME target) (fn proc => fn g =>
+      ctxt (SOME target) (fn proc => fn g =>
         fn card => fn genuine_only => fn size => g card genuine_only size
           |> (Option.map o apsnd o map) proc) t' []
   in
@@ -497,12 +496,11 @@
 
 fun compile_generator_exprs_raw ctxt ts =
   let
-    val thy = Proof_Context.theory_of ctxt
     val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts;
     val compiles = Code_Runtime.dynamic_value_strict
       (Counterexample_Batch.get, put_counterexample_batch,
         "Exhaustive_Generators.put_counterexample_batch")
-      thy (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
+      ctxt (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
       (HOLogic.mk_list @{typ "natural => term list option"} ts') []
   in
     map (fn compile => fn size => compile size
@@ -515,12 +513,11 @@
 
 fun compile_validator_exprs_raw ctxt ts =
   let
-    val thy = Proof_Context.theory_of ctxt
     val ts' = map (mk_validator_expr ctxt) ts
   in
     Code_Runtime.dynamic_value_strict
       (Validator_Batch.get, put_validator_batch, "Exhaustive_Generators.put_validator_batch")
-      thy (SOME target) (K I) (HOLogic.mk_list @{typ "natural => bool"} ts') []
+      ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural => bool"} ts') []
   end;
 
 fun compile_validator_exprs ctxt ts =
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Feb 26 11:57:52 2014 +0100
@@ -303,13 +303,12 @@
     with_tmp_dir tmp_prefix run
   end;
 
-fun dynamic_value_strict opts cookie thy postproc t =
+fun dynamic_value_strict opts cookie ctxt postproc t =
   let
-    val ctxt = Proof_Context.init_global thy
     fun evaluator program ((_, vs_ty), t) deps =
       Exn.interruptible_capture (value opts ctxt cookie)
-        (Code_Target.evaluator thy target program deps true (vs_ty, t));
-  in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
+        (Code_Target.evaluator ctxt target program deps true (vs_ty, t));
+  in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t) end;
 
 (** counterexample generator **)
 
@@ -462,7 +461,7 @@
         val execute = dynamic_value_strict (true, opts)
           ((K true, fn _ => error ""), (Existential_Counterexample.get, Existential_Counterexample.put,
             "Narrowing_Generators.put_existential_counterexample"))
-          thy (apfst o Option.map o map_counterexample)
+          ctxt (apfst o Option.map o map_counterexample)
       in  
         case act execute (mk_property qs prop_t) of 
           SOME (counterexample, result) => Quickcheck.Result
@@ -488,7 +487,7 @@
         val execute = dynamic_value_strict (false, opts)
           ((is_genuine, counterexample_of),
             (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample"))
-          thy (apfst o Option.map o apsnd o map)
+          ctxt (apfst o Option.map o apsnd o map)
       in
         case act execute (ensure_testable (finitize t')) of 
           SOME (counterexample, result) =>
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Feb 26 11:57:52 2014 +0100
@@ -406,7 +406,6 @@
     
 fun compile_generator_expr_raw ctxt ts =
   let
-    val thy = Proof_Context.theory_of ctxt
     val iterations = Config.get ctxt Quickcheck.iterations
   in
     if Config.get ctxt Quickcheck.report then
@@ -414,7 +413,7 @@
         val t' = mk_parametric_reporting_generator_expr ctxt ts;
         val compile = Code_Runtime.dynamic_value_strict
           (Counterexample_Report.get, put_counterexample_report, "Random_Generators.put_counterexample_report")
-          thy (SOME target)
+          ctxt (SOME target)
           (fn proc => fn g => fn c => fn b => fn s => g c b s
             #>> (apfst o Option.map o apsnd o map) proc) t' [];
         fun single_tester c b s = compile c b s |> Random_Engine.run
@@ -436,7 +435,7 @@
         val t' = mk_parametric_generator_expr ctxt ts;
         val compile = Code_Runtime.dynamic_value_strict
           (Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
-          thy (SOME target)
+          ctxt (SOME target)
           (fn proc => fn g => fn c => fn b => fn s => g c b s
             #>> (Option.map o apsnd o map) proc) t' [];
         fun single_tester c b s = compile c b s |> Random_Engine.run
--- a/src/HOL/Tools/code_evaluation.ML	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/Tools/code_evaluation.ML	Wed Feb 26 11:57:52 2014 +0100
@@ -6,14 +6,14 @@
 
 signature CODE_EVALUATION =
 sig
-  val dynamic_value: theory -> term -> term option
-  val dynamic_value_strict: theory -> term -> term
-  val dynamic_value_exn: theory -> term -> term Exn.result
-  val static_value: theory -> string list -> typ list -> term -> term option
-  val static_value_strict: theory -> string list -> typ list -> term -> term
-  val static_value_exn: theory -> string list -> typ list -> term -> term Exn.result
-  val dynamic_conv: theory -> conv
-  val static_conv: theory -> string list -> typ list -> conv
+  val dynamic_value: Proof.context -> term -> term option
+  val dynamic_value_strict: Proof.context -> term -> term
+  val dynamic_value_exn: Proof.context -> term -> term Exn.result
+  val static_value: Proof.context -> string list -> typ list -> Proof.context -> term -> term option
+  val static_value_strict: Proof.context -> string list -> typ list -> Proof.context -> term -> term
+  val static_value_exn: Proof.context -> string list -> typ list -> Proof.context -> term -> term Exn.result
+  val dynamic_conv: Proof.context -> conv
+  val static_conv: Proof.context -> string list -> typ list -> Proof.context -> conv
   val put_term: (unit -> term) -> Proof.context -> Proof.context
   val tracing: string -> 'a -> 'a
   val setup: theory -> theory
@@ -171,44 +171,48 @@
 
 fun term_of_const_for thy = Axclass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
 
-fun gen_dynamic_value dynamic_value thy t =
-  dynamic_value cookie thy NONE I (mk_term_of t) [];
+fun gen_dynamic_value dynamic_value ctxt t =
+  dynamic_value cookie ctxt NONE I (mk_term_of t) [];
 
 val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value;
 val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
 val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
 
-fun gen_static_value static_value thy consts Ts =
-  static_value cookie thy NONE I (union (op =) (map (term_of_const_for thy) Ts) consts)
-  o mk_term_of;
+fun gen_static_value static_value ctxt consts Ts =
+  let
+    val static_value' = static_value cookie ctxt NONE I
+      (union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts)
+  in fn ctxt' => fn t => static_value' ctxt' (mk_term_of t) end;
 
 val static_value = gen_static_value Code_Runtime.static_value;
 val static_value_strict = gen_static_value Code_Runtime.static_value_strict;
 val static_value_exn = gen_static_value Code_Runtime.static_value_exn;
 
-fun certify_eval thy value conv ct =
+fun certify_eval ctxt value conv ct =
   let
+    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
     val t = Thm.term_of ct;
     val T = fastype_of t;
-    val mk_eq = Thm.mk_binop (Thm.cterm_of thy (Const ("==", T --> T --> propT)));
-  in case value t
+    val mk_eq = Thm.mk_binop (cert (Const ("==", T --> T --> propT)));
+  in case value ctxt t
    of NONE => Thm.reflexive ct
-    | SOME t' => conv (mk_eq ct (Thm.cterm_of thy t')) RS @{thm eq_eq_TrueD}
+    | SOME t' => conv ctxt (mk_eq ct (cert t')) RS @{thm eq_eq_TrueD}
         handle THM _ =>
-          error ("Failed to certify evaluation result of " ^ Syntax.string_of_term_global thy t)
+          error ("Failed to certify evaluation result of " ^ Syntax.string_of_term ctxt t)
   end;
 
-fun dynamic_conv thy = certify_eval thy (dynamic_value thy)
-  (Code_Runtime.dynamic_holds_conv thy);
+fun dynamic_conv ctxt = certify_eval ctxt dynamic_value
+  Code_Runtime.dynamic_holds_conv;
 
-fun static_conv thy consts Ts =
+fun static_conv ctxt consts Ts =
   let
     val eqs = "==" :: @{const_name HOL.eq} ::
-      map (fn T => Axclass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
-        (*assumes particular code equations for "==" etc.*)
+      map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt)
+        (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for "==" etc.*)
+    val value = static_value ctxt consts Ts;
+    val holds = Code_Runtime.static_holds_conv ctxt (union (op =) eqs consts);
   in
-    certify_eval thy (static_value thy consts Ts)
-      (Code_Runtime.static_holds_conv thy (union (op =) eqs consts))
+    fn ctxt' => certify_eval ctxt' value holds
   end;
 
 
@@ -225,6 +229,6 @@
   #> Code.datatype_interpretation ensure_term_of_code
   #> Code.abstype_interpretation ensure_abs_term_of_code
   #> Context.theory_map (Syntax_Phases.term_check 0 "termify" check_termify)
-  #> Value.add_evaluator ("code", dynamic_value_strict o Proof_Context.theory_of);
+  #> Value.add_evaluator ("code", dynamic_value_strict);
 
 end;
--- a/src/Tools/Code/code_preproc.ML	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/Tools/Code/code_preproc.ML	Wed Feb 26 11:57:52 2014 +0100
@@ -10,27 +10,29 @@
   val map_pre: (Proof.context -> Proof.context) -> theory -> theory
   val map_post: (Proof.context -> Proof.context) -> theory -> theory
   val add_unfold: thm -> theory -> theory
-  val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
+  val add_functrans: string * (Proof.context -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
   val del_functrans: string -> theory -> theory
-  val simple_functrans: (theory -> thm list -> thm list option)
-    -> theory -> (thm * bool) list -> (thm * bool) list option
-  val print_codeproc: theory -> unit
+  val simple_functrans: (Proof.context -> thm list -> thm list option)
+    -> Proof.context -> (thm * bool) list -> (thm * bool) list option
+  val print_codeproc: Proof.context -> unit
 
   type code_algebra
   type code_graph
   val cert: code_graph -> string -> Code.cert
   val sortargs: code_graph -> string -> sort list
   val all: code_graph -> string list
-  val pretty: theory -> code_graph -> Pretty.T
+  val pretty: Proof.context -> code_graph -> Pretty.T
   val obtain: bool -> theory -> string list -> term list -> code_algebra * code_graph
-  val dynamic_conv: theory
+  val dynamic_conv: Proof.context
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
-  val dynamic_value: theory -> ((term -> term) -> 'a -> 'a)
+  val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a)
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
-  val static_conv: theory -> string list
-    -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
-  val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
-    -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
+  val static_conv: Proof.context -> string list
+    -> (code_algebra -> code_graph -> Proof.context -> (string * sort) list -> term -> conv)
+    -> Proof.context -> conv
+  val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list
+    -> (code_algebra -> code_graph -> Proof.context -> (string * sort) list -> term -> 'a)
+    -> Proof.context -> term -> 'a
 
   val setup: theory -> theory
 end
@@ -45,7 +47,7 @@
 datatype thmproc = Thmproc of {
   pre: simpset,
   post: simpset,
-  functrans: (string * (serial * (theory -> (thm * bool) list -> (thm * bool) list option))) list
+  functrans: (string * (serial * (Proof.context -> (thm * bool) list -> (thm * bool) list option))) list
 };
 
 fun make_thmproc ((pre, post), functrans) =
@@ -110,9 +112,10 @@
 
 (* post- and preprocessing *)
 
-fun no_variables_conv conv ct =
+fun no_variables_conv ctxt conv ct =
   let
-    val cert = Thm.cterm_of (Thm.theory_of_cterm ct);
+    val thy = Proof_Context.theory_of ctxt;
+    val cert = Thm.cterm_of thy;
     val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (cert t)
       | t as Var _ => insert (op aconvc) (cert t)
       | _ => I) (Thm.term_of ct) [];
@@ -128,48 +131,52 @@
 
 fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
 
-fun term_of_conv thy conv =
-  Thm.cterm_of thy
-  #> conv
+fun term_of_conv ctxt conv =
+  Thm.cterm_of (Proof_Context.theory_of ctxt)
+  #> conv ctxt
   #> Thm.prop_of
   #> Logic.dest_equals
   #> snd;
 
-fun term_of_conv_resubst thy conv t =
+fun term_of_conv_resubst ctxt conv t =
   let
     val all_vars = fold_aterms (fn t as Free _ => insert (op aconv) t
       | t as Var _ => insert (op aconv) t
       | _ => I) t [];
     val resubst = curry (Term.betapplys o swap) all_vars;
-  in (resubst, term_of_conv thy conv (fold_rev lambda all_vars t)) end;
-
-fun global_simpset_context thy ss =
-  Proof_Context.init_global thy
-  |> put_simpset ss;
+  in (resubst, term_of_conv ctxt conv (fold_rev lambda all_vars t)) end;
 
-fun preprocess_conv thy =
+fun preprocess_conv ctxt =
   let
-    val pre = global_simpset_context thy ((#pre o the_thmproc) thy);
-  in
-    Simplifier.rewrite pre
-    #> trans_conv_rule (Axclass.unoverload_conv thy)
+    val thy = Proof_Context.theory_of ctxt;
+    val ss = (#pre o the_thmproc) thy;
+  in fn ctxt' =>
+    Simplifier.rewrite (put_simpset ss ctxt')
+    #> trans_conv_rule (Axclass.unoverload_conv (Proof_Context.theory_of ctxt'))
   end;
 
-fun preprocess_term thy = term_of_conv_resubst thy (preprocess_conv thy);
-
-fun postprocess_conv thy =
+fun preprocess_term ctxt =
   let
-    val post = global_simpset_context thy ((#post o the_thmproc) thy);
-  in
-    Axclass.overload_conv thy
-    #> trans_conv_rule (Simplifier.rewrite post)
+    val conv = preprocess_conv ctxt;
+  in fn ctxt' => term_of_conv_resubst ctxt' conv end;
+
+fun postprocess_conv ctxt =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val ss = (#post o the_thmproc) thy;
+  in fn ctxt' =>
+    Axclass.overload_conv (Proof_Context.theory_of ctxt')
+    #> trans_conv_rule (Simplifier.rewrite (put_simpset ss ctxt'))
   end;
 
-fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
+fun postprocess_term ctxt =
+  let
+    val conv = postprocess_conv ctxt;
+  in fn ctxt' => term_of_conv ctxt' conv end;
 
-fun print_codeproc thy =
+fun print_codeproc ctxt =
   let
-    val ctxt = Proof_Context.init_global thy;
+    val thy = Proof_Context.theory_of ctxt;
     val pre = (#pre o the_thmproc) thy;
     val post = (#post o the_thmproc) thy;
     val functrans = (map fst o #functrans o the_thmproc) thy;
@@ -193,7 +200,7 @@
     ]
   end;
 
-fun simple_functrans f thy eqns = case f thy (map fst eqns)
+fun simple_functrans f ctxt eqns = case f ctxt (map fst eqns)
  of SOME thms' => SOME (map (rpair (forall snd eqns)) thms')
   | NONE => NONE;
 
@@ -210,12 +217,16 @@
 fun sortargs eqngr = map snd o fst o get_node eqngr;
 fun all eqngr = Graph.keys eqngr;
 
-fun pretty thy eqngr =
-  AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
-  |> (map o apfst) (Code.string_of_const thy)
-  |> sort (string_ord o pairself fst)
-  |> map (fn (s, cert) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: Code.pretty_cert thy cert))
-  |> Pretty.chunks;
+fun pretty ctxt eqngr =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+  in
+    AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
+    |> (map o apfst) (Code.string_of_const thy)
+    |> sort (string_ord o pairself fst)
+    |> map (fn (s, cert) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: Code.pretty_cert thy cert))
+    |> Pretty.chunks
+  end;
 
 
 (** the Waisenhaus algorithm **)
@@ -269,17 +280,18 @@
    of SOME (lhs, cert) => ((lhs, []), cert)
     | NONE => let
         val thy = Proof_Context.theory_of ctxt;
-        val functrans = (map (fn (_, (_, f)) => f thy)
+        val functrans = (map (fn (_, (_, f)) => f ctxt)
           o #functrans o the_thmproc) thy;
         val cert = Code.get_cert thy { functrans = functrans, ss = simpset_of ctxt } c; (*FIXME*)
         val (lhs, rhss) =
           Code.typargs_deps_of_cert thy cert;
       in ((lhs, rhss), cert) end;
 
-fun obtain_instance thy arities (inst as (class, tyco)) =
+fun obtain_instance ctxt arities (inst as (class, tyco)) =
   case AList.lookup (op =) arities inst
    of SOME classess => (classess, ([], []))
     | NONE => let
+        val thy = Proof_Context.theory_of ctxt;
         val all_classes = complete_proper_sort thy [class];
         val super_classes = remove (op =) class all_classes;
         val classess = map (complete_proper_sort thy)
@@ -331,7 +343,7 @@
   if member (op =) insts inst then vardeps_data
   else let
     val (classess, (super_classes, inst_params)) =
-      obtain_instance (Proof_Context.theory_of ctxt) arities inst;
+      obtain_instance ctxt arities inst;
   in
     vardeps_data
     |> (apsnd o apsnd) (insert (op =) inst)
@@ -381,8 +393,9 @@
 
 (* applying instantiations *)
 
-fun dicts_of thy (proj_sort, algebra) (T, sort) =
+fun dicts_of ctxt (proj_sort, algebra) (T, sort) =
   let
+    val thy = Proof_Context.theory_of ctxt;
     fun class_relation (x, _) _ = x;
     fun type_constructor (tyco, _) xs class =
       inst_params thy tyco (Sorts.complete_sort algebra [class])
@@ -395,14 +408,15 @@
        handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
   end;
 
-fun add_arity thy vardeps (class, tyco) =
+fun add_arity ctxt vardeps (class, tyco) =
   AList.default (op =) ((class, tyco),
     map_range (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
-      (Sign.arity_number thy tyco));
+      (Sign.arity_number (Proof_Context.theory_of ctxt) tyco));
 
-fun add_cert thy vardeps (c, (proto_lhs, proto_cert)) (rhss, eqngr) =
+fun add_cert ctxt vardeps (c, (proto_lhs, proto_cert)) (rhss, eqngr) =
   if can (Graph.get_node eqngr) c then (rhss, eqngr)
   else let
+    val thy = Proof_Context.theory_of ctxt;
     val lhs = map_index (fn (k, (v, _)) =>
       (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
     val cert = proto_cert
@@ -412,20 +426,21 @@
     val eqngr' = Graph.new_node (c, (vs, cert)) eqngr;
   in (map (pair c) rhss' @ rhss, eqngr') end;
 
-fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) =
+fun extend_arities_eqngr raw_ctxt cs ts (arities, (eqngr : code_graph)) =
   let
+    val thy = Proof_Context.theory_of raw_ctxt;
     val {pre, ...} = the_thmproc thy;
-    val ctxt = thy |> Proof_Context.init_global |> put_simpset pre;
+    val ctxt = put_simpset pre raw_ctxt;
     val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
       insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
     val (vardeps, (eqntab, insts)) = empty_vardeps_data
       |> fold (ensure_fun ctxt arities eqngr) cs
       |> fold (ensure_rhs ctxt arities eqngr) cs_rhss;
-    val arities' = fold (add_arity thy vardeps) insts arities;
+    val arities' = fold (add_arity ctxt vardeps) insts arities;
     val algebra = Sorts.subalgebra (Context.pretty_global thy) (is_proper_class thy)
       (AList.lookup (op =) arities') (Sign.classes_of thy);
-    val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr);
-    fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
+    val (rhss, eqngr') = Symtab.fold (add_cert ctxt vardeps) eqntab ([], eqngr);
+    fun deps_of (c, rhs) = c :: maps (dicts_of ctxt algebra)
       (rhs ~~ sortargs eqngr' c);
     val eqngr'' = fold (fn (c, rhs) => fold
       (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
@@ -444,59 +459,62 @@
 (** retrieval and evaluation interfaces **)
 
 fun obtain ignore_cache thy consts ts = apsnd snd
-  (Wellsorted.change_yield (if ignore_cache then NONE else SOME thy) (extend_arities_eqngr thy consts ts));
+  (Wellsorted.change_yield (if ignore_cache then NONE else SOME thy)
+    (extend_arities_eqngr (Proof_Context.init_global thy) consts ts));
 
 fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
 
-fun dynamic_conv thy conv = no_variables_conv (fn ct =>
+fun dynamic_conv ctxt conv = no_variables_conv ctxt (fn ct =>
   let
-    val thm1 = preprocess_conv thy ct;
+    val thm1 = preprocess_conv ctxt ctxt ct;
     val ct' = Thm.rhs_of thm1;
     val (vs', t') = dest_cterm ct';
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
-    val (algebra', eqngr') = obtain false thy consts [t'];
+    val (algebra', eqngr') = obtain false (Proof_Context.theory_of ctxt) consts [t'];
     val thm2 = conv algebra' eqngr' vs' t' ct';
-    val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
+    val thm3 = postprocess_conv ctxt ctxt (Thm.rhs_of thm2);
   in
     Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
       error ("could not construct evaluation proof:\n"
-      ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
+      ^ (cat_lines o map (Display.string_of_thm ctxt)) [thm1, thm2, thm3])
   end);
 
-fun dynamic_value thy postproc evaluator t =
+fun dynamic_value ctxt postproc evaluator t =
   let
-    val (resubst, t') = preprocess_term thy t;
+    val (resubst, t') = preprocess_term ctxt ctxt t;
     val vs' = Term.add_tfrees t' [];
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
-    val (algebra', eqngr') = obtain false thy consts [t'];
+    val (algebra', eqngr') = obtain false (Proof_Context.theory_of ctxt) consts [t'];
   in
     t'
     |> evaluator algebra' eqngr' vs'
-    |> postproc (postprocess_term thy o resubst)
+    |> postproc (postprocess_term ctxt ctxt o resubst)
   end;
 
-fun static_conv thy consts conv =
+fun static_conv ctxt consts conv =
   let
-    val (algebra, eqngr) = obtain true thy consts [];
+    val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
+    val pre_conv = preprocess_conv ctxt;
     val conv' = conv algebra eqngr;
-  in
-    no_variables_conv ((preprocess_conv thy)
-      then_conv (fn ct => uncurry conv' (dest_cterm ct) ct)
-      then_conv (postprocess_conv thy))
+    val post_conv = postprocess_conv ctxt;
+  in fn ctxt' => no_variables_conv ctxt' ((pre_conv ctxt')
+    then_conv (fn ct => uncurry (conv' ctxt') (dest_cterm ct) ct)
+    then_conv (post_conv ctxt'))
   end;
 
-fun static_value thy postproc consts evaluator =
+fun static_value ctxt postproc consts evaluator =
   let
-    val (algebra, eqngr) = obtain true thy consts [];
+    val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
+    val preproc = preprocess_term ctxt;
     val evaluator' = evaluator algebra eqngr;
-    val postproc' = postprocess_term thy;
-  in 
-    preprocess_term thy
+    val postproc' = postprocess_term ctxt;
+  in fn ctxt' => 
+    preproc ctxt'
     #-> (fn resubst => fn t => t
-      |> evaluator' (Term.add_tfrees t [])
-      |> postproc (postproc' o resubst))
+      |> evaluator' ctxt' (Term.add_tfrees t [])
+      |> postproc (postproc' ctxt' o resubst))
   end;
 
 
@@ -518,7 +536,6 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_codeproc"} "print code preprocessor setup"
-    (Scan.succeed (Toplevel.unknown_theory o
-      Toplevel.keep (print_codeproc o Toplevel.theory_of)));
+    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_codeproc o Toplevel.context_of)));
 
 end; (*struct*)
--- a/src/Tools/Code/code_runtime.ML	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML	Wed Feb 26 11:57:52 2014 +0100
@@ -11,20 +11,20 @@
     (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string ->
     string * string -> 'a
   type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
-  val dynamic_value: 'a cookie -> theory -> string option
+  val dynamic_value: 'a cookie -> Proof.context -> string option
     -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a option
-  val dynamic_value_strict: 'a cookie -> theory -> string option
+  val dynamic_value_strict: 'a cookie -> Proof.context -> string option
     -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a
-  val dynamic_value_exn: 'a cookie -> theory -> string option
+  val dynamic_value_exn: 'a cookie -> Proof.context -> string option
     -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result
-  val static_value: 'a cookie -> theory -> string option
-    -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a option
-  val static_value_strict: 'a cookie -> theory -> string option
-    -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a
-  val static_value_exn: 'a cookie -> theory -> string option
-    -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a Exn.result
-  val dynamic_holds_conv: theory -> conv
-  val static_holds_conv: theory -> string list -> conv
+  val static_value: 'a cookie -> Proof.context -> string option
+    -> ((term -> term) -> 'a -> 'a) -> string list -> Proof.context -> term -> 'a option
+  val static_value_strict: 'a cookie -> Proof.context -> string option
+    -> ((term -> term) -> 'a -> 'a) -> string list -> Proof.context -> term -> 'a
+  val static_value_exn: 'a cookie -> Proof.context -> string option
+    -> ((term -> term) -> 'a -> 'a) -> string list -> Proof.context -> term -> 'a Exn.result
+  val dynamic_holds_conv: Proof.context -> conv
+  val static_holds_conv: Proof.context -> string list -> Proof.context -> conv
   val code_reflect: (string * string list option) list -> string list -> string
     -> string option -> theory -> theory
   datatype truth = Holds
@@ -83,21 +83,19 @@
 
 type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
 
-fun reject_vars thy t =
-  let
-    val ctxt = Proof_Context.init_global thy;
-  in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
+fun reject_vars ctxt t =
+  ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t);
 
-fun obtain_evaluator thy some_target program consts expr =
-  Code_Target.evaluator thy (the_default target some_target) program consts false expr
-  |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
+fun obtain_evaluator ctxt some_target program consts =
+  let
+    val evaluator' = Code_Target.evaluator ctxt (the_default target some_target) program consts false;
+  in
+    evaluator'
+    #> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules))
+  end;
 
-fun obtain_evaluator' thy some_target program =
-  obtain_evaluator thy some_target program o map Constant;
-
-fun evaluation cookie thy evaluator vs_t args =
+fun evaluation cookie ctxt evaluator vs_t args =
   let
-    val ctxt = Proof_Context.init_global thy;
     val (program_code, value_name) = evaluator vs_t;
     val value_code = space_implode " "
       (value_name :: "()" :: map (enclose "(" ")") args);
@@ -108,36 +106,39 @@
     | General.Bind => NONE
     | General.Fail _ => NONE;
 
-fun dynamic_value_exn cookie thy some_target postproc t args =
+fun dynamic_value_exn cookie ctxt some_target postproc t args =
   let
-    val _ = reject_vars thy t;
+    val _ = reject_vars ctxt t;
     val _ = if ! trace
-      then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t))
+      then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t))
       else ()
     fun evaluator program ((_, vs_ty), t) deps =
-      evaluation cookie thy (obtain_evaluator thy some_target program deps) (vs_ty, t) args;
-  in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
+      evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) (vs_ty, t) args;
+  in Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t end;
 
-fun dynamic_value_strict cookie thy some_target postproc t args =
-  Exn.release (dynamic_value_exn cookie thy some_target postproc t args);
+fun dynamic_value_strict cookie ctxt some_target postproc t args =
+  Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args);
 
-fun dynamic_value cookie thy some_target postproc t args =
-  partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args);
+fun dynamic_value cookie ctxt some_target postproc t args =
+  partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args);
 
-fun static_evaluator cookie thy some_target program consts' =
+fun static_evaluator cookie ctxt some_target program consts' =
   let
-    val evaluator = obtain_evaluator' thy some_target program consts'
-  in fn ((_, vs_ty), t) => fn _ => evaluation cookie thy evaluator (vs_ty, t) [] end;
+    val evaluator = obtain_evaluator ctxt some_target program (map Constant consts');
+    val evaluation' = evaluation cookie ctxt evaluator;
+  in fn _ => fn ((_, vs_ty), t) => fn _ => evaluation' (vs_ty, t) [] end;
 
-fun static_value_exn cookie thy some_target postproc consts =
-  Code_Thingol.static_value thy (Exn.map_result o postproc) consts
-    (static_evaluator cookie thy some_target) o reject_vars thy;
+fun static_value_exn cookie ctxt some_target postproc consts =
+  let
+    val evaluator = Code_Thingol.static_value ctxt (Exn.map_result o postproc) consts
+      (static_evaluator cookie ctxt some_target);
+  in fn ctxt' => evaluator ctxt' o reject_vars ctxt' end;
 
-fun static_value_strict cookie thy some_target postproc consts =
-  Exn.release o static_value_exn cookie thy some_target postproc consts;
+fun static_value_strict cookie ctxt some_target postproc consts =
+  Exn.release oo static_value_exn cookie ctxt some_target postproc consts;
 
 fun static_value cookie thy some_target postproc consts =
-  partiality_as_none o static_value_exn cookie thy some_target postproc consts;
+  partiality_as_none oo static_value_exn cookie thy some_target postproc consts;
 
 
 (* evaluation for truth or nothing *)
@@ -151,18 +152,19 @@
 val put_truth = Truth_Result.put;
 val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");
 
-val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of);
+val reject_vars = fn ctxt => tap (reject_vars ctxt o Thm.term_of);
 
 local
 
-fun check_holds thy evaluator vs_t ct =
+fun check_holds ctxt evaluator vs_t ct =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val t = Thm.term_of ct;
     val _ = if fastype_of t <> propT
       then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
       else ();
     val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
-    val result = case partiality_as_none (evaluation truth_cookie thy evaluator vs_t [])
+    val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t [])
      of SOME Holds => true
       | _ => false;
   in
@@ -171,34 +173,39 @@
 
 val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (@{binding holds_by_evaluation},
-  fn (thy, evaluator, vs_t, ct) => check_holds thy evaluator vs_t ct)));
+  fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct)));
 
-fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct =
-  raw_check_holds_oracle (thy, evaluator, (vs_ty, t), ct);
+fun check_holds_oracle ctxt evaluator ((_, vs_ty), t) deps ct =
+  raw_check_holds_oracle (ctxt, evaluator, (vs_ty, t), ct);
 
 in
 
-fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
+fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt
   (fn program => fn vs_t => fn deps =>
-    check_holds_oracle thy (obtain_evaluator thy NONE program deps) vs_t deps)
-      o reject_vars thy;
+    check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t deps)
+      o reject_vars ctxt;
 
-fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts
-  (fn program => fn consts' =>
-    check_holds_oracle thy (obtain_evaluator' thy NONE program consts'))
-      o reject_vars thy;
+fun static_holds_conv ctxt consts =
+  Code_Thingol.static_conv ctxt consts (fn program => fn consts' =>
+    let
+      val evaluator' = obtain_evaluator ctxt NONE program (map Constant consts')
+    in
+      fn ctxt' => fn vs_t => fn deps => check_holds_oracle ctxt' evaluator' vs_t deps o reject_vars ctxt'
+    end);
+
+(* o reject_vars ctxt'*)
 
 end; (*local*)
 
 
 (** instrumentalization **)
 
-fun evaluation_code thy module_name tycos consts =
+fun evaluation_code ctxt module_name tycos consts =
   let
-    val ctxt = Proof_Context.init_global thy;
+    val thy = Proof_Context.theory_of ctxt;
     val program = Code_Thingol.consts_program thy consts;
     val (ml_modules, target_names) =
-      Code_Target.produce_code_for thy
+      Code_Target.produce_code_for ctxt
         target NONE module_name [] program false (map Constant consts @ map Type_Constructor tycos);
     val ml_code = space_implode "\n\n" (map snd ml_modules);
     val (consts', tycos') = chop (length consts) target_names;
@@ -234,7 +241,7 @@
     val tycos' = fold (insert (op =)) new_tycos tycos;
     val consts' = fold (insert (op =)) new_consts consts;
     val acc_code = Lazy.lazy (fn () =>
-      evaluation_code (Proof_Context.theory_of ctxt) structure_generated tycos' consts'
+      evaluation_code ctxt structure_generated tycos' consts'
       |> apsnd snd);
   in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
 
@@ -330,12 +337,13 @@
 
 fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy  =
   let
+    val ctxt = Proof_Context.init_global thy;
     val datatypes = map (fn (raw_tyco, raw_cos) =>
-      (prep_type thy raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes;
+      (prep_type ctxt raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes;
     val (tycos, constrs) = map_split (uncurry (check_datatype thy)) datatypes
       |> apsnd flat;
     val functions = map (prep_const thy) raw_functions;
-    val result = evaluation_code thy module_name tycos (constrs @ functions)
+    val result = evaluation_code ctxt module_name tycos (constrs @ functions)
       |> (apsnd o apsnd) (chop (length constrs));
   in
     thy
@@ -440,7 +448,7 @@
   |-> (fn ([Const (const, _)], _) =>
     Code_Target.set_printings (Constant (const,
       [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
-  #> tap (fn thy => Code_Target.produce_code thy false [const] target NONE structure_generated []));
+  #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target NONE structure_generated []));
 
 fun process_file filepath (definienda, thy) =
   let
--- a/src/Tools/Code/code_simp.ML	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/Tools/Code/code_simp.ML	Wed Feb 26 11:57:52 2014 +0100
@@ -7,11 +7,11 @@
 signature CODE_SIMP =
 sig
   val map_ss: (Proof.context -> Proof.context) -> theory -> theory
-  val dynamic_conv: theory -> conv
-  val dynamic_tac: theory -> int -> tactic
-  val dynamic_value: theory -> term -> term
-  val static_conv: theory -> simpset option -> string list -> conv
-  val static_tac: theory -> simpset option -> string list -> Proof.context -> int -> tactic
+  val dynamic_conv: Proof.context -> conv
+  val dynamic_tac: Proof.context -> int -> tactic
+  val dynamic_value: Proof.context -> term -> term
+  val static_conv: Proof.context -> simpset option -> string list -> Proof.context -> conv
+  val static_tac: Proof.context -> simpset option -> string list -> Proof.context -> int -> tactic
   val setup: theory -> theory
   val trace: bool Config.T
 end;
@@ -31,11 +31,11 @@
 
 fun map_ss f thy = Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy;
 
-fun simpset_default thy some_ss = the_default (Simpset.get thy) some_ss;
+fun simpset_default ctxt some_ss = the_default (Simpset.get (Proof_Context.theory_of ctxt)) some_ss;
 
-fun simp_ctxt_default thy some_ss =
-  Proof_Context.init_global thy
-  |> put_simpset (simpset_default thy some_ss);
+(*fun simp_ctxt_default ctxt some_ss =
+  Proof_Context.init_global ctxt
+  |> put_simpset (simpset_default ctxt some_ss);*)
 
 
 (* diagnostic *)
@@ -50,7 +50,7 @@
   end;
 
 
-(* build simpset and conversion from program *)
+(* build simpset context and conversion from program *)
 
 fun add_stmt (Code_Thingol.Fun ((_, eqs), some_cong)) ss =
       ss
@@ -63,43 +63,49 @@
 
 val add_program = Code_Symbol.Graph.fold (add_stmt o fst o snd);
 
-fun simp_ctxt_program thy some_ss program =
-  simp_ctxt_default thy some_ss
-  |> add_program program;
+fun simpset_program ctxt some_ss program =
+  simpset_map ctxt (add_program program) (simpset_default ctxt some_ss);
 
-fun rewrite_modulo thy some_ss program =
-  Simplifier.full_rewrite (simp_ctxt_program thy some_ss program |> set_trace);
+fun rewrite_modulo ctxt some_ss program =
+  let
+    val ss = simpset_program ctxt some_ss program;
+  in fn ctxt => Simplifier.full_rewrite (ctxt |> put_simpset ss |> set_trace) end;
 
-fun conclude_tac thy some_ss =
-  Simplifier.full_simp_tac o Simplifier.put_simpset (simpset_default thy some_ss);
+fun conclude_tac ctxt some_ss =
+  let
+    val ss = simpset_default ctxt some_ss
+  in fn ctxt => Simplifier.full_simp_tac (ctxt |> put_simpset ss) end;
 
 
 (* evaluation with dynamic code context *)
 
-fun dynamic_conv thy = Code_Thingol.dynamic_conv thy
-  (fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
+fun dynamic_conv ctxt = Code_Thingol.dynamic_conv ctxt
+  (fn program => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt);
 
-fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE (Proof_Context.init_global thy);
+fun dynamic_tac ctxt = CONVERSION (dynamic_conv ctxt)
+  THEN' conclude_tac ctxt NONE ctxt;
 
-fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy;
+fun dynamic_value ctxt =
+  snd o Logic.dest_equals o Thm.prop_of o dynamic_conv ctxt o Thm.cterm_of (Proof_Context.theory_of ctxt);
 
 val setup =
   Method.setup @{binding code_simp}
-    (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of)))
+    (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac)))
     "simplification with code equations"
-  #> Value.add_evaluator ("simp", dynamic_value o Proof_Context.theory_of);
+  #> Value.add_evaluator ("simp", dynamic_value);
 
 
 (* evaluation with static code context *)
 
-fun static_conv thy some_ss consts =
-  Code_Thingol.static_conv_simple thy consts
-    (fn program => fn _ => fn _ => rewrite_modulo thy some_ss program);
+fun static_conv ctxt some_ss consts =
+  Code_Thingol.static_conv_simple ctxt consts
+    (fn program => let val conv' = rewrite_modulo ctxt some_ss program
+     in fn ctxt' => fn _ => fn _ => conv' ctxt' end);
 
-fun static_tac thy some_ss consts =
+fun static_tac ctxt some_ss consts =
   let
-    val conv = static_conv thy some_ss consts;
-    val tac = conclude_tac thy some_ss;
-  in fn ctxt => CONVERSION conv THEN' tac ctxt end;
+    val conv = static_conv ctxt some_ss consts;
+    val tac = conclude_tac ctxt some_ss;
+  in fn ctxt' => CONVERSION (conv ctxt') THEN' (tac ctxt') end;
 
 end;
--- a/src/Tools/Code/code_target.ML	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Wed Feb 26 11:57:52 2014 +0100
@@ -6,29 +6,29 @@
 
 signature CODE_TARGET =
 sig
-  val cert_tyco: theory -> string -> string
-  val read_tyco: theory -> string -> string
+  val cert_tyco: Proof.context -> string -> string
+  val read_tyco: Proof.context -> string -> string
 
-  val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
+  val export_code_for: Proof.context -> Path.T option -> string -> int option -> string -> Token.T list
     -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
-  val produce_code_for: theory -> string -> int option -> string -> Token.T list
+  val produce_code_for: Proof.context -> string -> int option -> string -> Token.T list
     -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string * string) list * string option list
-  val present_code_for: theory -> string -> int option -> string -> Token.T list
+  val present_code_for: Proof.context -> string -> int option -> string -> Token.T list
     -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
-  val check_code_for: theory -> string -> bool -> Token.T list
+  val check_code_for: Proof.context -> string -> bool -> Token.T list
     -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
 
-  val export_code: theory -> bool -> string list
+  val export_code: Proof.context -> bool -> string list
     -> (((string * string) * Path.T option) * Token.T list) list -> unit
-  val produce_code: theory -> bool -> string list
+  val produce_code: Proof.context -> bool -> string list
     -> string -> int option -> string -> Token.T list -> (string * string) list * string option list
-  val present_code: theory -> string list -> Code_Symbol.T list
+  val present_code: Proof.context -> string list -> Code_Symbol.T list
     -> string -> int option -> string -> Token.T list -> string
-  val check_code: theory -> bool -> string list
+  val check_code: Proof.context -> bool -> string list
     -> ((string * bool) * Token.T list) list -> unit
 
   val generatedN: string
-  val evaluator: theory -> string -> Code_Thingol.program
+  val evaluator: Proof.context -> string -> Code_Thingol.program
     -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
     -> (string * string) list * string
 
@@ -40,8 +40,8 @@
   val extend_target: string *
       (string * (Code_Thingol.program -> Code_Thingol.program))
     -> theory -> theory
-  val assert_target: theory -> string -> string
-  val the_literals: theory -> string -> literals
+  val assert_target: Proof.context -> string -> string
+  val the_literals: Proof.context -> string -> literals
   type serialization
   val parse_args: 'a parser -> Token.T list -> 'a
   val serialization: (int -> Path.T option -> 'a -> unit)
@@ -83,45 +83,45 @@
 
 (** checking and parsing of symbols **)
 
-fun cert_const thy const =
+fun cert_const ctxt const =
   let
-    val _ = if Sign.declared_const thy const then ()
+    val _ = if Sign.declared_const (Proof_Context.theory_of ctxt) const then ()
       else error ("No such constant: " ^ quote const);
   in const end;
 
-fun cert_tyco thy tyco =
+fun read_const ctxt = Code.read_const (Proof_Context.theory_of ctxt);
+
+fun cert_tyco ctxt tyco =
   let
-    val _ = if Sign.declared_tyname thy tyco then ()
+    val _ = if Sign.declared_tyname (Proof_Context.theory_of ctxt) tyco then ()
       else error ("No such type constructor: " ^ quote tyco);
   in tyco end;
 
-fun read_tyco thy = #1 o dest_Type
-  o Proof_Context.read_type_name_proper (Proof_Context.init_global thy) true;
+fun read_tyco ctxt = #1 o dest_Type
+  o Proof_Context.read_type_name_proper ctxt true;
 
-fun cert_class thy class =
+fun cert_class ctxt class =
   let
-    val _ = Axclass.get_info thy class;
+    val _ = Axclass.get_info (Proof_Context.theory_of ctxt) class;
   in class end;
 
-fun read_class thy = Proof_Context.read_class (Proof_Context.init_global thy);
-
 val parse_classrel_ident = Parse.class --| @{keyword "<"} -- Parse.class;
 
-fun cert_inst thy (class, tyco) =
-  (cert_class thy class, cert_tyco thy tyco);
+fun cert_inst ctxt (class, tyco) =
+  (cert_class ctxt class, cert_tyco ctxt tyco);
 
-fun read_inst thy (raw_tyco, raw_class) =
-  (read_tyco thy raw_tyco, read_class thy raw_class);
+fun read_inst ctxt (raw_tyco, raw_class) =
+  (read_tyco ctxt raw_tyco, Proof_Context.read_class ctxt raw_class);
 
 val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class;
 
-fun cert_syms thy =
-  Code_Symbol.map_attr (apfst (cert_const thy)) (apfst (cert_tyco thy))
-    (apfst (cert_class thy)) ((apfst o pairself) (cert_class thy)) (apfst (cert_inst thy)) I;
+fun cert_syms ctxt =
+  Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt))
+    (apfst (cert_class ctxt)) ((apfst o pairself) (cert_class ctxt)) (apfst (cert_inst ctxt)) I;
 
-fun read_syms thy =
-  Code_Symbol.map_attr (apfst (Code.read_const thy)) (apfst (read_tyco thy))
-    (apfst (read_class thy)) ((apfst o pairself) (read_class thy)) (apfst (read_inst thy)) I;
+fun read_syms ctxt =
+  Code_Symbol.map_attr (apfst (read_const ctxt)) (apfst (read_tyco ctxt))
+    (apfst (Proof_Context.read_class ctxt)) ((apfst o pairself) (Proof_Context.read_class ctxt)) (apfst (read_inst ctxt)) I;
 
 fun check_name is_module s =
   let
@@ -231,7 +231,8 @@
     (Symtab.join (merge_target true) (target1, target2), Int.max (width1, width2));
 );
 
-fun assert_target thy target = if Symtab.defined (fst (Targets.get thy)) target
+fun assert_target ctxt target =
+  if Symtab.defined (fst (Targets.get (Proof_Context.theory_of ctxt))) target
   then target
   else error ("Unknown code target language: " ^ quote target);
 
@@ -264,7 +265,7 @@
 
 fun map_target_data target f thy =
   let
-    val _ = assert_target thy target;
+    val _ = assert_target (Proof_Context.init_global thy) target;
   in
     thy
     |> (Targets.map o apfst o Symtab.map_entry target o map_target o apsnd) f
@@ -284,9 +285,9 @@
 
 (* montage *)
 
-fun the_fundamental thy =
+fun the_fundamental ctxt =
   let
-    val (targets, _) = Targets.get thy;
+    val (targets, _) = Targets.get (Proof_Context.theory_of ctxt);
     fun fundamental target = case Symtab.lookup targets target
      of SOME data => (case the_description data
          of Fundamental data => data
@@ -294,11 +295,11 @@
       | NONE => error ("Unknown code target language: " ^ quote target);
   in fundamental end;
 
-fun the_literals thy = #literals o the_fundamental thy;
+fun the_literals ctxt = #literals o the_fundamental ctxt;
 
-fun collapse_hierarchy thy =
+fun collapse_hierarchy ctxt =
   let
-    val (targets, _) = Targets.get thy;
+    val (targets, _) = Targets.get (Proof_Context.theory_of ctxt);
     fun collapse target =
       let
         val data = case Symtab.lookup targets target
@@ -314,15 +315,15 @@
 
 local
 
-fun activate_target thy target =
+fun activate_target ctxt target =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val (_, default_width) = Targets.get thy;
-    val (modify, data) = collapse_hierarchy thy target;
+    val (modify, data) = collapse_hierarchy ctxt target;
   in (default_width, data, modify) end;
 
-fun project_program thy syms_hidden syms1 program2 =
+fun project_program ctxt syms_hidden syms1 program2 =
   let
-    val ctxt = Proof_Context.init_global thy;
     val syms2 = subtract (op =) syms_hidden syms1;
     val program3 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program2;
     val syms4 = Code_Symbol.Graph.all_succs program3 syms2;
@@ -334,17 +335,17 @@
     val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3;
   in (syms4, program4) end;
 
-fun prepare_serializer thy (serializer : serializer) reserved identifiers
+fun prepare_serializer ctxt (serializer : serializer) reserved identifiers
     printings module_name args proto_program syms =
   let
     val syms_hidden = Code_Symbol.symbols_of printings;
-    val (syms_all, program) = project_program thy syms_hidden syms proto_program;
+    val (syms_all, program) = project_program ctxt syms_hidden syms proto_program;
     fun select_include (name, (content, cs)) =
       if null cs orelse exists (fn c => member (op =) syms_all (Constant c)) cs
       then SOME (name, content) else NONE;
     val includes = map_filter select_include (Code_Symbol.dest_module_data printings);
   in
-    (serializer args (Proof_Context.init_global thy) {
+    (serializer args ctxt {
       module_name = module_name,
       reserved_syms = reserved,
       identifiers = identifiers,
@@ -355,62 +356,62 @@
       (syms_all, program))
   end;
 
-fun mount_serializer thy target some_width module_name args program syms =
+fun mount_serializer ctxt target some_width module_name args program syms =
   let
-    val (default_width, data, modify) = activate_target thy target;
+    val (default_width, data, modify) = activate_target ctxt target;
     val serializer = case the_description data
      of Fundamental seri => #serializer seri;
     val (prepared_serializer, (prepared_syms, prepared_program)) =
-      prepare_serializer thy serializer
+      prepare_serializer ctxt serializer
         (the_reserved data) (the_identifiers data) (the_printings data)
         module_name args (modify program) syms
     val width = the_default default_width some_width;
   in (fn program => fn syms => prepared_serializer syms program width, (prepared_syms, prepared_program)) end;
 
-fun invoke_serializer thy target some_width raw_module_name args program all_public syms =
+fun invoke_serializer ctxt target some_width raw_module_name args program all_public syms =
   let
     val module_name = if raw_module_name = "" then ""
       else (check_name true raw_module_name; raw_module_name)
-    val (mounted_serializer, (prepared_syms, prepared_program)) = mount_serializer thy
-      target some_width module_name args program syms;
+    val (mounted_serializer, (prepared_syms, prepared_program)) =
+      mount_serializer ctxt target some_width module_name args program syms;
   in mounted_serializer prepared_program (if all_public then prepared_syms else []) end;
 
 fun assert_module_name "" = error "Empty module name not allowed here"
   | assert_module_name module_name = module_name;
 
-fun using_master_directory thy =
-  Option.map (Path.append (File.pwd ()) o Path.append (Thy_Load.master_directory thy));
+fun using_master_directory ctxt =
+  Option.map (Path.append (File.pwd ()) o Path.append (Thy_Load.master_directory (Proof_Context.theory_of ctxt)));
 
 in
 
 val generatedN = "Generated_Code";
 
-fun export_code_for thy some_path target some_width module_name args =
-  export (using_master_directory thy some_path)
-  ooo invoke_serializer thy target some_width module_name args;
+fun export_code_for ctxt some_path target some_width module_name args =
+  export (using_master_directory ctxt some_path)
+  ooo invoke_serializer ctxt target some_width module_name args;
 
-fun produce_code_for thy target some_width module_name args =
+fun produce_code_for ctxt target some_width module_name args =
   let
-    val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
+    val serializer = invoke_serializer ctxt target some_width (assert_module_name module_name) args;
   in fn program => fn all_public => fn syms =>
     produce (serializer program all_public syms) |> apsnd (fn deresolve => map deresolve syms)
   end;
 
-fun present_code_for thy target some_width module_name args =
+fun present_code_for ctxt target some_width module_name args =
   let
-    val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
+    val serializer = invoke_serializer ctxt target some_width (assert_module_name module_name) args;
   in fn program => fn (syms, selects) =>
     present selects (serializer program false syms)
   end;
 
-fun check_code_for thy target strict args program all_public syms =
+fun check_code_for ctxt target strict args program all_public syms =
   let
     val { env_var, make_destination, make_command } =
-      (#check o the_fundamental thy) target;
+      (#check o the_fundamental ctxt) target;
     fun ext_check p =
       let
         val destination = make_destination p;
-        val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
+        val _ = export (SOME destination) (invoke_serializer ctxt target (SOME 80)
           generatedN args program all_public syms);
         val cmd = make_command generatedN;
       in
@@ -443,10 +444,10 @@
     val value_name = the (deresolve Code_Symbol.value);
   in (program_code, value_name) end;
 
-fun evaluator thy target program syms =
+fun evaluator ctxt target program syms =
   let
     val (mounted_serializer, (_, prepared_program)) =
-      mount_serializer thy target NONE generatedN [] program syms;
+      mount_serializer ctxt target NONE generatedN [] program syms;
   in evaluation mounted_serializer prepared_program syms end;
 
 end; (* local *)
@@ -457,60 +458,66 @@
 fun prep_destination "" = NONE
   | prep_destination s = SOME (Path.explode s);
 
-fun export_code thy all_public cs seris =
+fun export_code ctxt all_public cs seris =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val program = Code_Thingol.consts_program thy cs;
     val _ = map (fn (((target, module_name), some_path), args) =>
-      export_code_for thy some_path target NONE module_name args program all_public (map Constant cs)) seris;
+      export_code_for ctxt some_path target NONE module_name args program all_public (map Constant cs)) seris;
   in () end;
 
-fun export_code_cmd all_public raw_cs seris thy =
-  export_code thy all_public
-    (Code_Thingol.read_const_exprs thy raw_cs)
+fun export_code_cmd all_public raw_cs seris ctxt =
+  export_code ctxt all_public
+    (Code_Thingol.read_const_exprs ctxt raw_cs)
     ((map o apfst o apsnd) prep_destination seris);
 
-fun produce_code thy all_public cs target some_width some_module_name args =
+fun produce_code ctxt all_public cs target some_width some_module_name args =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val program = Code_Thingol.consts_program thy cs;
-  in produce_code_for thy target some_width some_module_name args program all_public (map Constant cs) end;
+  in produce_code_for ctxt target some_width some_module_name args program all_public (map Constant cs) end;
 
-fun present_code thy cs syms target some_width some_module_name args =
+fun present_code ctxt cs syms target some_width some_module_name args =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val program = Code_Thingol.consts_program thy cs;
-  in present_code_for thy target some_width some_module_name args program (map Constant cs, syms) end;
+  in present_code_for ctxt target some_width some_module_name args program (map Constant cs, syms) end;
 
-fun check_code thy all_public cs seris =
+fun check_code ctxt all_public cs seris =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val program = Code_Thingol.consts_program thy cs;
     val _ = map (fn ((target, strict), args) =>
-      check_code_for thy target strict args program all_public (map Constant cs)) seris;
+      check_code_for ctxt target strict args program all_public (map Constant cs)) seris;
   in () end;
 
-fun check_code_cmd all_public raw_cs seris thy =
-  check_code thy all_public
-    (Code_Thingol.read_const_exprs thy raw_cs) seris;
+fun check_code_cmd all_public raw_cs seris ctxt =
+  check_code ctxt all_public
+    (Code_Thingol.read_const_exprs ctxt raw_cs) seris;
 
 local
 
 val parse_const_terms = Scan.repeat1 Args.term
-  >> (fn ts => fn thy => map (Code.check_const thy) ts);
+  >> (fn ts => fn ctxt => map (Code.check_const (Proof_Context.theory_of ctxt)) ts);
 
 fun parse_names category parse internalize mark_symbol =
   Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
-  >> (fn xs => fn thy => map (mark_symbol o internalize thy) xs);
+  >> (fn xs => fn ctxt => map (mark_symbol o internalize ctxt) xs);
 
 val parse_consts = parse_names "consts" Args.term
-  Code.check_const Constant;
+  (Code.check_const o Proof_Context.theory_of) Constant;
 
 val parse_types = parse_names "types" (Scan.lift Args.name)
-  Sign.intern_type Type_Constructor;
+  (Sign.intern_type o Proof_Context.theory_of) Type_Constructor;
 
 val parse_classes = parse_names "classes" (Scan.lift Args.name)
-  Sign.intern_class Type_Class;
+  (Sign.intern_class o Proof_Context.theory_of) Type_Class;
 
 val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
-  (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class))
-    Class_Instance;
+  (fn ctxt => fn (raw_tyco, raw_class) =>
+    let
+      val thy = Proof_Context.theory_of ctxt;
+    in (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class) end) Class_Instance;
 
 in
 
@@ -520,11 +527,9 @@
       Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
       -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
     (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
-      let val thy = Proof_Context.theory_of ctxt in
-        present_code thy (mk_cs thy)
-          (maps (fn f => f thy) mk_stmtss)
-          target some_width "Example" []
-      end);
+        present_code ctxt (mk_cs ctxt)
+          (maps (fn f => f ctxt) mk_stmtss)
+          target some_width "Example" []);
 
 end;
 
@@ -535,7 +540,7 @@
 
 fun add_reserved target sym thy =
   let
-    val (_, data) = collapse_hierarchy thy target;
+    val (_, data) = collapse_hierarchy (Proof_Context.init_global thy) target;
     val _ = if member (op =) (the_reserved data) sym
       then error ("Reserved symbol " ^ quote sym ^ " already declared")
       else ();
@@ -547,13 +552,13 @@
 
 (* checking of syntax *)
 
-fun check_const_syntax thy target c syn =
-  if Code_Printer.requires_args syn > Code.args_number thy c
+fun check_const_syntax ctxt target c syn =
+  if Code_Printer.requires_args syn > Code.args_number (Proof_Context.theory_of ctxt) c
   then error ("Too many arguments in syntax for constant " ^ quote c)
-  else Code_Printer.prep_const_syntax thy (the_literals thy target) c syn;
+  else Code_Printer.prep_const_syntax (Proof_Context.theory_of ctxt) (the_literals ctxt target) c syn;
 
-fun check_tyco_syntax thy target tyco syn =
-  if fst syn <> Sign.arity_number thy tyco
+fun check_tyco_syntax ctxt target tyco syn =
+  if fst syn <> Sign.arity_number (Proof_Context.theory_of ctxt) tyco
   then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
   else syn;
 
@@ -569,14 +574,14 @@
       (arrange false) (arrange false) (arrange true) x
   end;
 
-fun cert_name_decls thy = cert_syms thy #> arrange_name_decls;
+fun cert_name_decls ctxt = cert_syms ctxt #> arrange_name_decls;
 
-fun read_name_decls thy = read_syms thy #> arrange_name_decls;
+fun read_name_decls ctxt = read_syms ctxt #> arrange_name_decls;
 
 fun set_identifier (target, sym_name) = map_identifiers target (Code_Symbol.set_data sym_name);
 
 fun gen_set_identifiers prep_name_decl raw_name_decls thy =
-  fold set_identifier (prep_name_decl thy raw_name_decls) thy;
+  fold set_identifier (prep_name_decl (Proof_Context.init_global thy) raw_name_decls) thy;
 
 val set_identifiers = gen_set_identifiers cert_name_decls;
 val set_identifiers_cmd = gen_set_identifiers read_name_decls;
@@ -584,26 +589,26 @@
 
 (* custom printings *)
 
-fun arrange_printings prep_const thy =
+fun arrange_printings prep_const ctxt =
   let
     fun arrange check (sym, target_syns) =
-      map (fn (target, some_syn) => (target, (sym, Option.map (check thy target sym) some_syn))) target_syns;
+      map (fn (target, some_syn) => (target, (sym, Option.map (check ctxt target sym) some_syn))) target_syns;
   in
     Code_Symbol.maps_attr'
       (arrange check_const_syntax) (arrange check_tyco_syntax)
         (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I))
-        (arrange (fn thy => fn _ => fn _ => fn (raw_content, raw_cs) =>
-          (Code_Printer.str raw_content, map (prep_const thy) raw_cs)))
+        (arrange (fn ctxt => fn _ => fn _ => fn (raw_content, raw_cs) =>
+          (Code_Printer.str raw_content, map (prep_const ctxt) raw_cs)))
   end;
 
-fun cert_printings thy = cert_syms thy #> arrange_printings cert_const thy;
+fun cert_printings ctxt = cert_syms ctxt #> arrange_printings cert_const ctxt;
 
-fun read_printings thy = read_syms thy #> arrange_printings Code.read_const thy;
+fun read_printings ctxt = read_syms ctxt #> arrange_printings read_const ctxt;
 
 fun set_printing (target, sym_syn) = map_printings target (Code_Symbol.set_data sym_syn);
 
 fun gen_set_printings prep_print_decl raw_print_decls thy =
-  fold set_printing (prep_print_decl thy raw_print_decls) thy;
+  fold set_printing (prep_print_decl (Proof_Context.init_global thy) raw_print_decls) thy;
 
 val set_printings = gen_set_printings cert_printings;
 val set_printings_cmd = gen_set_printings read_printings;
@@ -680,18 +685,18 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
-    (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
+    (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.context_of)));
 
 
 (** external entrance point -- for codegen tool **)
 
 fun codegen_tool thyname cmd_expr =
   let
-    val thy = Thy_Info.get_theory thyname;
+    val ctxt = Proof_Context.init_global (Thy_Info.get_theory thyname);
     val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
       (filter Token.is_proper o Outer_Syntax.scan Position.none);
   in case parse cmd_expr
-   of SOME f => (writeln "Now generating code..."; f thy)
+   of SOME f => (writeln "Now generating code..."; f ctxt)
     | NONE => error ("Bad directive " ^ quote cmd_expr)
   end;
 
--- a/src/Tools/Code/code_thingol.ML	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML	Wed Feb 26 11:57:52 2014 +0100
@@ -79,27 +79,28 @@
   val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
   val is_constr: program -> Code_Symbol.T -> bool
   val is_case: stmt -> bool
-  val group_stmts: theory -> program
+  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: theory -> string list -> string list
+  val read_const_exprs: Proof.context -> string list -> string list
   val consts_program: theory -> string list -> program
-  val dynamic_conv: theory -> (program
+  val dynamic_conv: Proof.context -> (program
     -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
     -> conv
-  val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (program
+  val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program
     -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
     -> term -> 'a
-  val static_conv: theory -> string list -> (program -> string list
-    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
-    -> conv
-  val static_conv_simple: theory -> string list
-    -> (program -> (string * sort) list -> term -> conv) -> conv
-  val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
+  val static_conv: Proof.context -> string list -> (program -> string list
+    -> Proof.context -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
+    -> Proof.context -> conv
+  val static_conv_simple: Proof.context -> string list
+    -> (program -> Proof.context -> (string * sort) list -> term -> conv)
+    -> Proof.context -> conv
+  val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list ->
     (program -> string list
-      -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
-    -> term -> 'a
+      -> Proof.context -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
+    -> Proof.context -> term -> 'a
 end;
 
 structure Code_Thingol: CODE_THINGOL =
@@ -334,7 +335,7 @@
   rev (Code_Symbol.Graph.strong_conn program)
   |> map (AList.make (Code_Symbol.Graph.get_node program));
 
-fun group_stmts thy program =
+fun group_stmts ctxt program =
   let
     fun is_fun (_, Fun _) = true | is_fun _ = false;
     fun is_datatypecons (_, Datatypecons _) = true | is_datatypecons _ = false;
@@ -351,8 +352,7 @@
       else if forall (is_fun orf is_classinst) stmts
       then ([], [], List.partition is_fun stmts)
       else error ("Illegal mutual dependencies: " ^ (commas
-        o map (Code_Symbol.quote (Proof_Context.init_global thy)
-        o fst)) stmts);
+        o map (Code_Symbol.quote ctxt o fst)) stmts);
   in
     linear_stmts program
     |> map group
@@ -388,12 +388,11 @@
 
 exception PERMISSIVE of unit;
 
-fun translation_error thy program permissive some_thm deps msg sub_msg =
+fun translation_error ctxt program permissive some_thm deps msg sub_msg =
   if permissive
   then raise PERMISSIVE ()
   else
     let
-      val ctxt = Proof_Context.init_global thy;
       val thm_msg =
         Option.map (fn thm => "in code equation " ^ Display.string_of_thm ctxt thm) some_thm;
       val dep_msg = if null (tl deps) then NONE
@@ -409,14 +408,14 @@
 fun maybe_permissive f prgrm =
   f prgrm |>> SOME handle PERMISSIVE () => (NONE, prgrm);
 
-fun not_wellsorted thy program permissive some_thm deps ty sort e =
+fun not_wellsorted ctxt program permissive some_thm deps ty sort e =
   let
-    val err_class = Sorts.class_error (Context.pretty_global thy) e;
+    val err_class = Sorts.class_error (Context.pretty ctxt) e;
     val err_typ =
-      "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort " ^
-        Syntax.string_of_sort_global thy sort;
+      "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
+        Syntax.string_of_sort ctxt sort;
   in
-    translation_error thy program permissive some_thm deps
+    translation_error ctxt program permissive some_thm deps
       "Wellsortedness error" (err_typ ^ "\n" ^ err_class)
   end;
 
@@ -442,25 +441,25 @@
       | tag (Free _) (t as Free _) = t
       | tag (Var _) (t as Var _) = t
       | tag (Bound _) (t as Bound _) = t;
-  in
-    tag
-  end
+  in tag end
 
-fun annotate thy algbr eqngr (c, ty) args rhs =
+fun annotate ctxt algbr eqngr (c, ty) args rhs =
   let
-    val ctxt = Proof_Context.init_global thy |> Config.put Type_Infer_Context.const_sorts false
-    val erase = map_types (fn _ => Type_Infer.anyT [])
-    val reinfer = singleton (Type_Infer_Context.infer_types ctxt)
-    val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args)
-    val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))))
+    val erase = map_types (fn _ => Type_Infer.anyT []);
+    val reinfer = singleton (Type_Infer_Context.infer_types ctxt);
+    val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args);
+    val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))));
+  in tag_term algbr eqngr reinferred_rhs rhs end
+
+fun annotate_eqns ctxt algbr eqngr (c, ty) eqns =
+  let
+    val ctxt' = ctxt |> Proof_Context.theory_of |> Proof_Context.init_global
+      |> Config.put Type_Infer_Context.const_sorts false;
+      (*avoid spurious fixed variables: there is no eigen context for equations*)
   in
-    tag_term algbr eqngr reinferred_rhs rhs
-  end
-
-fun annotate_eqns thy algbr eqngr (c, ty) eqns = 
-  map (apfst (fn (args, (rhs, some_abs)) => (args,
-    (annotate thy algbr eqngr (c, ty) args rhs, some_abs)))) eqns
-
+    map (apfst (fn (args, (rhs, some_abs)) => (args,
+      (annotate ctxt' algbr eqngr (c, ty) args rhs, some_abs)))) eqns
+  end;
 
 (* abstract dictionary construction *)
 
@@ -470,7 +469,7 @@
     Global of (string * class) * typarg_witness list list
   | Local of string * (int * sort);
 
-fun construct_dictionaries thy (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) =
+fun construct_dictionaries ctxt (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) =
   let
     fun class_relation ((Weakening (classrels, x)), sub_class) super_class =
       Weakening ((sub_class, super_class) :: classrels, x);
@@ -484,42 +483,44 @@
       {class_relation = K (Sorts.classrel_derivation algebra class_relation),
        type_constructor = type_constructor,
        type_variable = type_variable} (ty, proj_sort sort)
-      handle Sorts.CLASS_ERROR e => not_wellsorted thy program permissive some_thm deps ty sort e;
+      handle Sorts.CLASS_ERROR e => not_wellsorted ctxt program permissive some_thm deps ty sort e;
   in (typarg_witnesses, (deps, program)) end;
 
 
 (* translation *)
 
-fun ensure_tyco thy algbr eqngr permissive tyco =
+fun ensure_tyco ctxt algbr eqngr permissive tyco =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val ((vs, cos), _) = Code.get_type thy tyco;
     val stmt_datatype =
-      fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
+      fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs
       #>> map fst
       ##>> fold_map (fn (c, (vs, tys)) =>
-        ensure_const thy algbr eqngr permissive c
+        ensure_const ctxt algbr eqngr permissive c
         ##>> pair (map (unprefix "'" o fst) vs)
-        ##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
+        ##>> fold_map (translate_typ ctxt algbr eqngr permissive) tys) cos
       #>> Datatype;
   in ensure_stmt Type_Constructor stmt_datatype tyco end
-and ensure_const thy algbr eqngr permissive c =
+and ensure_const ctxt algbr eqngr permissive c =
   let
+    val thy = Proof_Context.theory_of ctxt;
     fun stmt_datatypecons tyco =
-      ensure_tyco thy algbr eqngr permissive tyco
+      ensure_tyco ctxt algbr eqngr permissive tyco
       #>> Datatypecons;
     fun stmt_classparam class =
-      ensure_class thy algbr eqngr permissive class
+      ensure_class ctxt algbr eqngr permissive class
       #>> Classparam;
     fun stmt_fun cert = case Code.equations_of_cert thy cert
      of (_, NONE) => pair NoStmt
       | ((vs, ty), SOME eqns) =>
           let
-            val eqns' = annotate_eqns thy algbr eqngr (c, ty) eqns
+            val eqns' = annotate_eqns ctxt algbr eqngr (c, ty) eqns
             val some_case_cong = Code.get_case_cong thy c;
           in
-            fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
-            ##>> translate_typ thy algbr eqngr permissive ty
-            ##>> translate_eqns thy algbr eqngr permissive eqns'
+            fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs
+            ##>> translate_typ ctxt algbr eqngr permissive ty
+            ##>> translate_eqns ctxt algbr eqngr permissive eqns'
             #>>
              (fn (_, NONE) => NoStmt
                | (tyscm, SOME eqns) => Fun ((tyscm, eqns), some_case_cong))
@@ -530,26 +531,28 @@
          of SOME class => stmt_classparam class
           | NONE => stmt_fun (Code_Preproc.cert eqngr c))
   in ensure_stmt Constant stmt_const c end
-and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
+and ensure_class ctxt (algbr as (_, algebra)) eqngr permissive class =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
     val cs = #params (Axclass.get_info thy class);
     val stmt_class =
       fold_map (fn super_class =>
-        ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
-      ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
-        ##>> translate_typ thy algbr eqngr permissive ty) cs
+        ensure_classrel ctxt algbr eqngr permissive (class, super_class)) super_classes
+      ##>> fold_map (fn (c, ty) => ensure_const ctxt algbr eqngr permissive c
+        ##>> translate_typ ctxt algbr eqngr permissive ty) cs
       #>> (fn info => Class (unprefix "'" Name.aT, info))
   in ensure_stmt Type_Class stmt_class class end
-and ensure_classrel thy algbr eqngr permissive (sub_class, super_class) =
+and ensure_classrel ctxt algbr eqngr permissive (sub_class, super_class) =
   let
     val stmt_classrel =
-      ensure_class thy algbr eqngr permissive sub_class
-      ##>> ensure_class thy algbr eqngr permissive super_class
+      ensure_class ctxt algbr eqngr permissive sub_class
+      ##>> ensure_class ctxt algbr eqngr permissive super_class
       #>> Classrel;
   in ensure_stmt Class_Relation stmt_classrel (sub_class, super_class) end
-and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (tyco, class) =
+and ensure_inst ctxt (algbr as (_, algebra)) eqngr permissive (tyco, class) =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
     val these_class_params = these o try (#params o Axclass.get_info thy);
     val class_params = these_class_params class;
@@ -562,8 +565,8 @@
     val arity_typ = Type (tyco, map TFree vs);
     val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
     fun translate_super_instance super_class =
-      ensure_class thy algbr eqngr permissive super_class
-      ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class])
+      ensure_class ctxt algbr eqngr permissive super_class
+      ##>> translate_dicts ctxt algbr eqngr permissive NONE (arity_typ, [super_class])
       #>> (fn (super_class, [Dict ([], Dict_Const (_, dss))]) => (super_class, dss));
     fun translate_classparam_instance (c, ty) =
       let
@@ -573,14 +576,14 @@
         val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
           o Logic.dest_equals o Thm.prop_of) thm;
       in
-        ensure_const thy algbr eqngr permissive c
-        ##>> translate_const thy algbr eqngr permissive (SOME thm) (const, NONE)
+        ensure_const ctxt algbr eqngr permissive c
+        ##>> translate_const ctxt algbr eqngr permissive (SOME thm) (const, NONE)
         #>> (fn (c, IConst const') => ((c, (const', dom_length)), (thm, true)))
       end;
     val stmt_inst =
-      ensure_class thy algbr eqngr permissive class
-      ##>> ensure_tyco thy algbr eqngr permissive tyco
-      ##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
+      ensure_class ctxt algbr eqngr permissive class
+      ##>> ensure_tyco ctxt algbr eqngr permissive tyco
+      ##>> fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs
       ##>> fold_map translate_super_instance super_classes
       ##>> fold_map translate_classparam_instance class_params
       ##>> fold_map translate_classparam_instance superclass_params
@@ -588,69 +591,72 @@
           Classinst { class = class, tyco = tyco, vs = vs,
             superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params });
   in ensure_stmt Class_Instance stmt_inst (tyco, class) end
-and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
+and translate_typ ctxt algbr eqngr permissive (TFree (v, _)) =
       pair (ITyVar (unprefix "'" v))
-  | translate_typ thy algbr eqngr permissive (Type (tyco, tys)) =
-      ensure_tyco thy algbr eqngr permissive tyco
-      ##>> fold_map (translate_typ thy algbr eqngr permissive) tys
+  | translate_typ ctxt algbr eqngr permissive (Type (tyco, tys)) =
+      ensure_tyco ctxt algbr eqngr permissive tyco
+      ##>> fold_map (translate_typ ctxt algbr eqngr permissive) tys
       #>> (fn (tyco, tys) => tyco `%% tys)
-and translate_term thy algbr eqngr permissive some_thm (Const (c, ty), some_abs) =
-      translate_app thy algbr eqngr permissive some_thm (((c, ty), []), some_abs)
-  | translate_term thy algbr eqngr permissive some_thm (Free (v, _), some_abs) =
+and translate_term ctxt algbr eqngr permissive some_thm (Const (c, ty), some_abs) =
+      translate_app ctxt algbr eqngr permissive some_thm (((c, ty), []), some_abs)
+  | translate_term ctxt algbr eqngr permissive some_thm (Free (v, _), some_abs) =
       pair (IVar (SOME v))
-  | translate_term thy algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
+  | translate_term ctxt algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
       let
         val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize false v, ty, t);
         val v'' = if member (op =) (Term.add_free_names t' []) v'
           then SOME v' else NONE
       in
-        translate_typ thy algbr eqngr permissive ty
-        ##>> translate_term thy algbr eqngr permissive some_thm (t', some_abs)
+        translate_typ ctxt algbr eqngr permissive ty
+        ##>> translate_term ctxt algbr eqngr permissive some_thm (t', some_abs)
         #>> (fn (ty, t) => (v'', ty) `|=> t)
       end
-  | translate_term thy algbr eqngr permissive some_thm (t as _ $ _, some_abs) =
+  | translate_term ctxt algbr eqngr permissive some_thm (t as _ $ _, some_abs) =
       case strip_comb t
        of (Const (c, ty), ts) =>
-            translate_app thy algbr eqngr permissive some_thm (((c, ty), ts), some_abs)
+            translate_app ctxt algbr eqngr permissive some_thm (((c, ty), ts), some_abs)
         | (t', ts) =>
-            translate_term thy algbr eqngr permissive some_thm (t', some_abs)
-            ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
+            translate_term ctxt algbr eqngr permissive some_thm (t', some_abs)
+            ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts
             #>> (fn (t, ts) => t `$$ ts)
-and translate_eqn thy algbr eqngr permissive ((args, (rhs, some_abs)), (some_thm, proper)) =
-  fold_map (translate_term thy algbr eqngr permissive some_thm) args
-  ##>> translate_term thy algbr eqngr permissive some_thm (rhs, some_abs)
+and translate_eqn ctxt algbr eqngr permissive ((args, (rhs, some_abs)), (some_thm, proper)) =
+  fold_map (translate_term ctxt algbr eqngr permissive some_thm) args
+  ##>> translate_term ctxt algbr eqngr permissive some_thm (rhs, some_abs)
   #>> rpair (some_thm, proper)
-and translate_eqns thy algbr eqngr permissive eqns =
-  maybe_permissive (fold_map (translate_eqn thy algbr eqngr permissive) eqns)
-and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) (deps, program) =
+and translate_eqns ctxt algbr eqngr permissive eqns =
+  maybe_permissive (fold_map (translate_eqn ctxt algbr eqngr permissive) eqns)
+and translate_const ctxt algbr eqngr permissive some_thm ((c, ty), some_abs) (deps, program) =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
         andalso Code.is_abstr thy c
-        then translation_error thy program permissive some_thm deps
+        then translation_error ctxt program permissive some_thm deps
           "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
       else ()
-  in translate_const_proper thy algbr eqngr permissive some_thm (c, ty) (deps, program) end
-and translate_const_proper thy algbr eqngr permissive some_thm (c, ty) =
+  in translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) (deps, program) end
+and translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val (annotate, ty') = dest_tagged_type ty;
     val typargs = Sign.const_typargs thy (c, ty');
     val sorts = Code_Preproc.sortargs eqngr c;
     val (dom, range) = Term.strip_type ty';
   in
-    ensure_const thy algbr eqngr permissive c
-    ##>> fold_map (translate_typ thy algbr eqngr permissive) typargs
-    ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (typargs ~~ sorts)
-    ##>> fold_map (translate_typ thy algbr eqngr permissive) (range :: dom)
+    ensure_const ctxt algbr eqngr permissive c
+    ##>> fold_map (translate_typ ctxt algbr eqngr permissive) typargs
+    ##>> fold_map (translate_dicts ctxt algbr eqngr permissive some_thm) (typargs ~~ sorts)
+    ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (range :: dom)
     #>> (fn (((c, typargs), dss), range :: dom) =>
       IConst { sym = Constant c, typargs = typargs, dicts = dss,
         dom = dom, range = range, annotate = annotate })
   end
-and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
-  translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
-  ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
+and translate_app_const ctxt algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
+  translate_const ctxt algbr eqngr permissive some_thm (c_ty, some_abs)
+  ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts
   #>> (fn (t, ts) => t `$$ ts)
-and translate_case thy algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
+and translate_case ctxt algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val undefineds = Code.undefineds thy;
     fun arg_types num_args ty = fst (chop num_args (binder_types ty));
     val tys = arg_types num_args (snd c_ty);
@@ -696,53 +702,53 @@
                 (case_pats ~~ ts_clause)));
       in ICase { term = t, typ = ty, clauses = clauses, primitive = t_app `$$ ts } end;
   in
-    translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
-    ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
+    translate_const ctxt algbr eqngr permissive some_thm (c_ty, NONE)
+    ##>> fold_map (fn (constr, n) => translate_const ctxt algbr eqngr permissive some_thm (constr, NONE)
       #>> rpair n) constrs
-    ##>> translate_typ thy algbr eqngr permissive ty
-    ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
+    ##>> translate_typ ctxt algbr eqngr permissive ty
+    ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts
     #>> (fn (((t, constrs), ty), ts) =>
       casify constrs ty t ts)
   end
-and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
+and translate_app_case ctxt algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
   if length ts < num_args then
     let
       val k = length ts;
       val tys = (take (num_args - k) o drop k o fst o strip_type) ty;
-      val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
-      val vs = Name.invent_names ctxt "a" tys;
+      val names = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
+      val vs = Name.invent_names names "a" tys;
     in
-      fold_map (translate_typ thy algbr eqngr permissive) tys
-      ##>> translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts @ map Free vs)
+      fold_map (translate_typ ctxt algbr eqngr permissive) tys
+      ##>> translate_case ctxt algbr eqngr permissive some_thm case_scheme ((c, ty), ts @ map Free vs)
       #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
     end
   else if length ts > num_args then
-    translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), take num_args ts)
-    ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) (drop num_args ts)
+    translate_case ctxt algbr eqngr permissive some_thm case_scheme ((c, ty), take num_args ts)
+    ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) (drop num_args ts)
     #>> (fn (t, ts) => t `$$ ts)
   else
-    translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts)
-and translate_app thy algbr eqngr permissive some_thm (c_ty_ts as ((c, _), _), some_abs) =
-  case Code.get_case_scheme thy c
-   of SOME case_scheme => translate_app_case thy algbr eqngr permissive some_thm case_scheme c_ty_ts
-    | NONE => translate_app_const thy algbr eqngr permissive some_thm (c_ty_ts, some_abs)
-and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr permissive (v, sort) =
-  fold_map (ensure_class thy algbr eqngr permissive) (proj_sort sort)
+    translate_case ctxt algbr eqngr permissive some_thm case_scheme ((c, ty), ts)
+and translate_app ctxt algbr eqngr permissive some_thm (c_ty_ts as ((c, _), _), some_abs) =
+  case Code.get_case_scheme (Proof_Context.theory_of ctxt) c
+   of SOME case_scheme => translate_app_case ctxt algbr eqngr permissive some_thm case_scheme c_ty_ts
+    | NONE => translate_app_const ctxt algbr eqngr permissive some_thm (c_ty_ts, some_abs)
+and translate_tyvar_sort ctxt (algbr as (proj_sort, _)) eqngr permissive (v, sort) =
+  fold_map (ensure_class ctxt algbr eqngr permissive) (proj_sort sort)
   #>> (fn sort => (unprefix "'" v, sort))
-and translate_dicts thy algbr eqngr permissive some_thm (ty, sort) =
+and translate_dicts ctxt algbr eqngr permissive some_thm (ty, sort) =
   let
     fun mk_dict (Weakening (classrels, x)) =
-          fold_map (ensure_classrel thy algbr eqngr permissive) classrels
+          fold_map (ensure_classrel ctxt algbr eqngr permissive) classrels
           ##>> mk_plain_dict x
           #>> Dict 
     and mk_plain_dict (Global (inst, dss)) =
-          ensure_inst thy algbr eqngr permissive inst
+          ensure_inst ctxt algbr eqngr permissive inst
           ##>> (fold_map o fold_map) mk_dict dss
           #>> (fn (inst, dss) => Dict_Const (inst, dss))
       | mk_plain_dict (Local (v, (n, sort))) =
           pair (Dict_Var (unprefix "'" v, (n, length sort)))
   in
-    construct_dictionaries thy algbr permissive some_thm (ty, sort)
+    construct_dictionaries ctxt algbr permissive some_thm (ty, sort)
     #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses)
   end;
 
@@ -758,7 +764,7 @@
 fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing =
   Program.change_yield (if ignore_cache then NONE else SOME thy)
     (fn program => ([], program)
-      |> generate thy algebra eqngr thing
+      |> generate (Proof_Context.init_global thy) algebra eqngr thing
       |-> (fn thing => fn (_, program) => (thing, program)));
 
 
@@ -766,8 +772,8 @@
 
 fun consts_program_internal thy permissive consts =
   let
-    fun generate_consts thy algebra eqngr =
-      fold_map (ensure_const thy algebra eqngr permissive);
+    fun generate_consts ctxt algebra eqngr =
+      fold_map (ensure_const ctxt algebra eqngr permissive);
   in
     invoke_generation permissive thy (Code_Preproc.obtain false thy consts [])
       generate_consts consts
@@ -789,17 +795,17 @@
 
 (* value evaluation *)
 
-fun ensure_value thy algbr eqngr t =
+fun ensure_value ctxt algbr eqngr t =
   let
     val ty = fastype_of t;
     val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
       o dest_TFree))) t [];
-    val t' = annotate thy algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
+    val t' = annotate ctxt algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
     val dummy_constant = Constant @{const_name dummy_pattern};
     val stmt_value =
-      fold_map (translate_tyvar_sort thy algbr eqngr false) vs
-      ##>> translate_typ thy algbr eqngr false ty
-      ##>> translate_term thy algbr eqngr false NONE (t', NONE)
+      fold_map (translate_tyvar_sort ctxt algbr eqngr false) vs
+      ##>> translate_typ ctxt algbr eqngr false ty
+      ##>> translate_term ctxt algbr eqngr false NONE (t', NONE)
       #>> (fn ((vs, ty), t) => Fun
         (((vs, ty), [(([], t), (NONE, true))]), NONE));
     fun term_value (deps, program1) =
@@ -820,62 +826,61 @@
 fun original_sorts vs =
   map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v));
 
-fun dynamic_evaluator thy evaluator algebra eqngr vs t =
+fun dynamic_evaluator ctxt evaluator algebra eqngr vs t =
   let
     val ((program, (((vs', ty'), t'), deps)), _) =
-      invoke_generation false thy (algebra, eqngr) ensure_value t;
+      invoke_generation false (Proof_Context.theory_of ctxt) (algebra, eqngr) ensure_value t;
   in evaluator program ((original_sorts vs vs', (vs', ty')), t') deps end;
 
-fun dynamic_conv thy evaluator =
-  Code_Preproc.dynamic_conv thy (dynamic_evaluator thy evaluator);
+fun dynamic_conv ctxt conv =
+  Code_Preproc.dynamic_conv ctxt (dynamic_evaluator ctxt conv);
 
-fun dynamic_value thy postproc evaluator =
-  Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator);
+fun dynamic_value ctxt postproc evaluator =
+  Code_Preproc.dynamic_value ctxt postproc (dynamic_evaluator ctxt evaluator);
 
-fun lift_evaluation thy evaluation' algebra eqngr program vs t =
+fun lift_evaluation ctxt evaluation algebra eqngr program vs t =
   let
     val ((_, (((vs', ty'), t'), deps)), _) =
-      ensure_value thy algebra eqngr t ([], program);
-  in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end;
+      ensure_value ctxt algebra eqngr t ([], program);
+  in evaluation ctxt ((original_sorts vs vs', (vs', ty')), t') deps end;
 
-fun lift_evaluator thy evaluator' consts algebra eqngr =
+fun lift_evaluator ctxt evaluator consts algebra eqngr =
   let
-    fun generate_consts thy algebra eqngr =
-      fold_map (ensure_const thy algebra eqngr false);
+    fun generate_consts ctxt algebra eqngr =
+      fold_map (ensure_const ctxt algebra eqngr false);
     val (consts', program) =
-      invoke_generation true thy (algebra, eqngr) generate_consts consts;
-    val evaluation' = evaluator' program consts';
-  in lift_evaluation thy evaluation' algebra eqngr program end;
+      invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
+    val evaluation = evaluator program consts';
+  in fn ctxt' => lift_evaluation ctxt' evaluation algebra eqngr program end;
 
-fun lift_evaluator_simple thy evaluator' consts algebra eqngr =
+fun lift_evaluator_simple ctxt evaluator consts algebra eqngr =
   let
-    fun generate_consts thy algebra eqngr =
-      fold_map (ensure_const thy algebra eqngr false);
+    fun generate_consts ctxt algebra eqngr =
+      fold_map (ensure_const ctxt algebra eqngr false);
     val (_, program) =
-      invoke_generation true thy (algebra, eqngr) generate_consts consts;
-  in evaluator' program end;
+      invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
+  in evaluator program end;
 
-fun static_conv thy consts conv =
-  Code_Preproc.static_conv thy consts (lift_evaluator thy conv consts);
+fun static_conv ctxt consts conv =
+  Code_Preproc.static_conv ctxt consts (lift_evaluator ctxt conv consts);
 
-fun static_conv_simple thy consts conv =
-  Code_Preproc.static_conv thy consts (lift_evaluator_simple thy conv consts);
+fun static_conv_simple ctxt consts conv =
+  Code_Preproc.static_conv ctxt consts (lift_evaluator_simple ctxt conv consts);
 
-fun static_value thy postproc consts evaluator =
-  Code_Preproc.static_value thy postproc consts (lift_evaluator thy evaluator consts);
+fun static_value ctxt postproc consts evaluator =
+  Code_Preproc.static_value ctxt postproc consts (lift_evaluator ctxt evaluator consts);
 
 
 (** constant expressions **)
 
-fun read_const_exprs_internal thy =
+fun read_const_exprs_internal ctxt =
   let
+    val thy = Proof_Context.theory_of ctxt;
     fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
       ((snd o #constants o Consts.dest o Sign.consts_of) thy') [];
     fun belongs_here thy' c = forall
       (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
     fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
-
-    val ctxt = Proof_Context.init_global thy;
     fun read_const_expr str =
       (case Syntax.parse_token ctxt (K NONE) Markup.empty (SOME o Symbol_Pos.implode o #1) str of
         SOME "_" => ([], consts_of thy)
@@ -886,28 +891,30 @@
       | NONE => ([Code.read_const thy str], []));
   in pairself flat o split_list o map read_const_expr end;
 
-fun read_const_exprs_all thy = op @ o read_const_exprs_internal thy;
+fun read_const_exprs_all ctxt = op @ o read_const_exprs_internal ctxt;
 
-fun read_const_exprs thy const_exprs =
+fun read_const_exprs ctxt const_exprs =
   let
-    val (consts, consts_permissive) = read_const_exprs_internal thy const_exprs;
-    val consts' = implemented_deps (consts_program_permissive thy consts_permissive);
+    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);
   in union (op =) consts' consts end;
 
 
 (** diagnostic commands **)
 
-fun code_depgr thy consts =
+fun code_depgr ctxt consts =
   let
-    val (_, eqngr) = Code_Preproc.obtain true thy consts [];
+    val (_, eqngr) = Code_Preproc.obtain true ((Proof_Context.theory_of ctxt)) consts [];
     val all_consts = Graph.all_succs eqngr consts;
   in Graph.restrict (member (op =) all_consts) eqngr end;
 
-fun code_thms thy = Pretty.writeln o Code_Preproc.pretty thy o code_depgr thy;
+fun code_thms ctxt = Pretty.writeln o Code_Preproc.pretty ctxt o code_depgr ctxt;
 
-fun code_deps thy consts =
+fun code_deps ctxt consts =
   let
-    val eqngr = code_depgr thy consts;
+    val thy = Proof_Context.theory_of ctxt;
+    val eqngr = code_depgr ctxt consts;
     val constss = Graph.strong_conn eqngr;
     val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
       Symtab.update (const, consts)) consts) constss;
@@ -926,8 +933,8 @@
 
 local
 
-fun code_thms_cmd thy = code_thms thy o read_const_exprs_all thy;
-fun code_deps_cmd thy = code_deps thy o read_const_exprs_all thy;
+fun code_thms_cmd ctxt = code_thms ctxt o read_const_exprs_all ctxt;
+fun code_deps_cmd ctxt = code_deps ctxt o read_const_exprs_all ctxt;
 
 in
 
@@ -935,15 +942,15 @@
   Outer_Syntax.improper_command @{command_spec "code_thms"}
     "print system of code equations for code"
     (Scan.repeat1 Parse.term >> (fn cs =>
-      Toplevel.unknown_theory o
-      Toplevel.keep (fn state => code_thms_cmd (Toplevel.theory_of state) cs)));
+      Toplevel.unknown_context o
+      Toplevel.keep (fn state => code_thms_cmd (Toplevel.context_of state) cs)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "code_deps"}
     "visualize dependencies of code equations for code"
     (Scan.repeat1 Parse.term >> (fn cs =>
-      Toplevel.unknown_theory o
-      Toplevel.keep (fn state => code_deps_cmd (Toplevel.theory_of state) cs)));
+      Toplevel.unknown_context o
+      Toplevel.keep (fn state => code_deps_cmd (Toplevel.context_of state) cs)));
 
 end;
 
--- a/src/Tools/nbe.ML	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/Tools/nbe.ML	Wed Feb 26 11:57:52 2014 +0100
@@ -6,10 +6,10 @@
 
 signature NBE =
 sig
-  val dynamic_conv: theory -> conv
-  val dynamic_value: theory -> term -> term
-  val static_conv: theory -> string list -> conv
-  val static_value: theory -> string list -> term -> term
+  val dynamic_conv: Proof.context -> conv
+  val dynamic_value: Proof.context -> term -> term
+  val static_conv: Proof.context -> string list -> Proof.context -> conv
+  val static_value: Proof.context -> string list -> Proof.context -> term -> term
 
   datatype Univ =
       Const of int * Univ list               (*named (uninterpreted) constants*)
@@ -83,8 +83,9 @@
 
 in
 
-fun lift_triv_classes_conv thy conv ct =
+fun lift_triv_classes_conv ctxt conv ct =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val algebra = Sign.classes_of thy;
     val certT = Thm.ctyp_of thy;
     val triv_classes = get_triv_classes thy;
@@ -128,8 +129,9 @@
     |> strip_of_class
   end;
 
-fun lift_triv_classes_rew thy rew t =
+fun lift_triv_classes_rew ctxt rew t =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val algebra = Sign.classes_of thy;
     val triv_classes = get_triv_classes thy;
     val vs = Term.add_tfrees t [];
@@ -388,10 +390,9 @@
 
 (* compile equations *)
 
-fun compile_eqnss thy nbe_program raw_deps [] = []
-  | compile_eqnss thy nbe_program raw_deps eqnss =
+fun compile_eqnss ctxt nbe_program raw_deps [] = []
+  | compile_eqnss ctxt nbe_program raw_deps eqnss =
       let
-        val ctxt = Proof_Context.init_global thy;
         val (deps, deps_vals) = split_list (map_filter
           (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Code_Symbol.Graph.get_node nbe_program dep)))) raw_deps);
         val idx_of = raw_deps
@@ -453,7 +454,7 @@
   else (Code_Symbol.Graph.new_node (name, (NONE, maxidx)) nbe_program,
     (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab));
 
-fun compile_stmts thy stmts_deps =
+fun compile_stmts ctxt stmts_deps =
   let
     val names = map (fst o fst) stmts_deps;
     val names_deps = map (fn ((name, _), deps) => (name, deps)) stmts_deps;
@@ -463,7 +464,7 @@
       |> distinct (op =)
       |> fold (insert (op =)) names;
     fun compile nbe_program = eqnss
-      |> compile_eqnss thy nbe_program refl_deps
+      |> compile_eqnss ctxt nbe_program refl_deps
       |> rpair nbe_program;
   in
     fold ensure_const_idx refl_deps
@@ -472,12 +473,12 @@
       #-> fold (fn (name, univ) => (Code_Symbol.Graph.map_node name o apfst) (K (SOME univ))))
   end;
 
-fun compile_program thy program =
+fun compile_program ctxt program =
   let
     fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Code_Symbol.Graph.get_node) nbe_program) names
       then (nbe_program, (maxidx, idx_tab))
       else (nbe_program, (maxidx, idx_tab))
-        |> compile_stmts thy (map (fn name => ((name, Code_Symbol.Graph.get_node program name),
+        |> compile_stmts ctxt (map (fn name => ((name, Code_Symbol.Graph.get_node program name),
           Code_Symbol.Graph.immediate_succs program name)) names);
   in
     fold_rev add_stmts (Code_Symbol.Graph.strong_conn program)
@@ -488,12 +489,12 @@
 
 (* term evaluation by compilation *)
 
-fun compile_term thy nbe_program deps (vs : (string * sort) list, t) =
+fun compile_term ctxt nbe_program deps (vs : (string * sort) list, t) =
   let 
     val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
   in
     (Code_Symbol.value, (vs, [([], t)]))
-    |> singleton (compile_eqnss thy nbe_program deps)
+    |> singleton (compile_eqnss ctxt nbe_program deps)
     |> snd
     |> (fn t => apps t (rev dict_frees))
   end;
@@ -506,7 +507,7 @@
   | typ_of_itype vs (ITyVar v) =
       TFree ("'" ^ v, (the o AList.lookup (op =) vs) v);
 
-fun term_of_univ thy (idx_tab : Code_Symbol.T Inttab.table) t =
+fun term_of_univ ctxt (idx_tab : Code_Symbol.T Inttab.table) t =
   let
     fun take_until f [] = []
       | take_until f (x :: xs) = if f x then [] else x :: take_until f xs;
@@ -527,7 +528,7 @@
             val const = const_of_idx idx;
             val T = map_type_tvar (fn ((v, i), _) =>
               Type_Infer.param typidx (v ^ string_of_int i, []))
-                (Sign.the_const_type thy const);
+                (Sign.the_const_type (Proof_Context.theory_of ctxt) const);
             val typidx' = typidx + 1;
           in of_apps bounds (Term.Const (const, T), ts') typidx' end
       | of_univ bounds (BVar (n, ts)) typidx =
@@ -541,9 +542,9 @@
 
 (* evaluation with type reconstruction *)
 
-fun eval_term thy (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
+fun eval_term raw_ctxt (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
   let
-    val ctxt = Syntax.init_pretty_global thy;
+    val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
     val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
     val ty' = typ_of_itype vs0 ty;
     fun type_infer t =
@@ -553,8 +554,8 @@
       if null (Term.add_tvars t []) then t
       else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
   in
-    compile_term thy nbe_program deps (vs, t)
-    |> term_of_univ thy idx_tab
+    compile_term ctxt nbe_program deps (vs, t)
+    |> term_of_univ ctxt idx_tab
     |> traced (fn t => "Normalized:\n" ^ string_of_term t)
     |> type_infer
     |> traced (fn t => "Types inferred:\n" ^ string_of_term t)
@@ -571,18 +572,19 @@
   val empty = (Code_Symbol.Graph.empty, (0, Inttab.empty));
 );
 
-fun compile ignore_cache thy program =
+fun compile ignore_cache ctxt program =
   let
     val (nbe_program, (_, idx_tab)) =
-      Nbe_Functions.change (if ignore_cache then NONE else SOME thy)
-        (compile_program thy program);
+      Nbe_Functions.change (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
+        (compile_program ctxt program);
   in (nbe_program, idx_tab) end;
 
 
 (* evaluation oracle *)
 
-fun mk_equals thy lhs raw_rhs =
+fun mk_equals ctxt lhs raw_rhs =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val ty = Thm.typ_of (Thm.ctyp_of_term lhs);
     val eq = Thm.cterm_of thy (Term.Const ("==", ty --> ty --> propT));
     val rhs = Thm.cterm_of thy raw_rhs;
@@ -590,28 +592,33 @@
 
 val (_, raw_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (@{binding normalization_by_evaluation},
-    fn (thy, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
-      mk_equals thy ct (eval_term thy nbe_program_idx_tab vsp_ty_t deps))));
+    fn (ctxt, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
+      mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab vsp_ty_t deps))));
+
+fun oracle ctxt nbe_program_idx_tab vsp_ty_t deps ct =
+  raw_oracle (ctxt, nbe_program_idx_tab, vsp_ty_t, deps, ct);
 
-fun oracle thy nbe_program_idx_tab vsp_ty_t deps ct =
-  raw_oracle (thy, nbe_program_idx_tab, vsp_ty_t, deps, ct);
+fun dynamic_conv ctxt = lift_triv_classes_conv ctxt
+  (Code_Thingol.dynamic_conv ctxt (oracle ctxt o compile false ctxt));
 
-fun dynamic_conv thy = lift_triv_classes_conv thy
-  (Code_Thingol.dynamic_conv thy (oracle thy o compile false thy));
+fun dynamic_value ctxt = lift_triv_classes_rew ctxt
+  (Code_Thingol.dynamic_value ctxt I (eval_term ctxt o compile false ctxt));
 
-fun dynamic_value thy = lift_triv_classes_rew thy
-  (Code_Thingol.dynamic_value thy I (eval_term thy o compile false thy));
+fun static_conv ctxt consts =
+  let
+    val evaluator = Code_Thingol.static_conv ctxt consts
+      (fn program => fn _ => K (oracle ctxt (compile true ctxt program)));
+  in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end;
 
-fun static_conv thy consts = lift_triv_classes_conv thy
-  (Code_Thingol.static_conv thy consts (K o oracle thy o compile true thy));
-
-fun static_value thy consts = lift_triv_classes_rew thy
-  (Code_Thingol.static_value thy I consts (K o eval_term thy o compile true thy));
+fun static_value ctxt consts =
+  let
+    val evaluator = Code_Thingol.static_value ctxt I consts
+      (fn program => fn _ => K (eval_term ctxt (compile true ctxt program)));
+  in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
 
 
 (** setup **)
 
-val setup = Value.add_evaluator ("nbe", dynamic_value o Proof_Context.theory_of);
+val setup = Value.add_evaluator ("nbe", dynamic_value);
 
 end;
- 
\ No newline at end of file