--- 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
--- 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;
--- 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;