# HG changeset patch
# User wenzelm
# Date 1436395189 -7200
# Node ID e266d5463e9dfe592034d5cdec5adfe0da618703
# Parent  8304fb4fb823e21a0852f2e983c1d33c5a5e85a9
clarified context;

diff -r 8304fb4fb823 -r e266d5463e9d src/Doc/more_antiquote.ML
--- a/src/Doc/more_antiquote.ML	Wed Jul 08 21:33:00 2015 +0200
+++ b/src/Doc/more_antiquote.ML	Thu Jul 09 00:39:49 2015 +0200
@@ -25,7 +25,7 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val const = Code.check_const thy raw_const;
-    val (_, eqngr) = Code_Preproc.obtain true thy [const] [];
+    val (_, eqngr) = Code_Preproc.obtain true ctxt [const] [];
     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
     val thms = Code_Preproc.cert eqngr const
       |> Code.equations_of_cert thy
diff -r 8304fb4fb823 -r e266d5463e9d src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Wed Jul 08 21:33:00 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML	Thu Jul 09 00:39:49 2015 +0200
@@ -21,7 +21,7 @@
   val sortargs: code_graph -> string -> sort list
   val all: code_graph -> string list
   val pretty: Proof.context -> code_graph -> Pretty.T
-  val obtain: bool -> theory -> string list -> term list -> code_algebra * code_graph
+  val obtain: bool -> Proof.context -> string list -> term list -> code_algebra * code_graph
   val dynamic_conv: Proof.context
     -> (code_algebra -> code_graph -> term -> conv) -> conv
   val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'b)
@@ -536,15 +536,15 @@
 
 (** 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 (Proof_Context.init_global thy) consts ts));
+fun obtain ignore_cache ctxt consts ts = apsnd snd
+  (Wellsorted.change_yield (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
+    (extend_arities_eqngr ctxt consts ts));
 
 fun dynamic_evaluator eval ctxt t =
   let
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t [];
-    val (algebra, eqngr) = obtain false (Proof_Context.theory_of ctxt) consts [t];
+    val (algebra, eqngr) = obtain false ctxt consts [t];
   in eval algebra eqngr t end;
 
 fun dynamic_conv ctxt conv =
@@ -555,12 +555,12 @@
 
 fun static_conv { ctxt, consts } conv =
   let
-    val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
+    val (algebra, eqngr) = obtain true ctxt consts [];
   in Sandwich.conversion (value_sandwich ctxt) (conv { algebra = algebra, eqngr = eqngr }) end;
 
 fun static_value { ctxt, lift_postproc, consts } evaluator =
   let
-    val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
+    val (algebra, eqngr) = obtain true ctxt consts [];
   in Sandwich.evaluation (value_sandwich ctxt) lift_postproc (evaluator { algebra = algebra, eqngr = eqngr }) end;
 
 
diff -r 8304fb4fb823 -r e266d5463e9d src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Jul 08 21:33:00 2015 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu Jul 09 00:39:49 2015 +0200
@@ -790,7 +790,8 @@
     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 [])
+    invoke_generation permissive thy
+      (Code_Preproc.obtain false (Proof_Context.init_global thy) consts [])
       generate_consts consts
     |> snd
   end;
@@ -918,7 +919,7 @@
 
 fun code_depgr ctxt consts =
   let
-    val (_, eqngr) = Code_Preproc.obtain true ((Proof_Context.theory_of ctxt)) consts [];
+    val (_, eqngr) = Code_Preproc.obtain true ctxt consts [];
     val all_consts = Graph.all_succs eqngr consts;
   in Graph.restrict (member (op =) all_consts) eqngr end;