clarified context;
authorwenzelm
Thu Jul 09 00:39:49 2015 +0200 (2015-07-09)
changeset 60697e266d5463e9d
parent 60696 8304fb4fb823
child 60698 29e8bdc41f90
clarified context;
src/Doc/more_antiquote.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Doc/more_antiquote.ML	Wed Jul 08 21:33:00 2015 +0200
     1.2 +++ b/src/Doc/more_antiquote.ML	Thu Jul 09 00:39:49 2015 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    let
     1.5      val thy = Proof_Context.theory_of ctxt;
     1.6      val const = Code.check_const thy raw_const;
     1.7 -    val (_, eqngr) = Code_Preproc.obtain true thy [const] [];
     1.8 +    val (_, eqngr) = Code_Preproc.obtain true ctxt [const] [];
     1.9      fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
    1.10      val thms = Code_Preproc.cert eqngr const
    1.11        |> Code.equations_of_cert thy
     2.1 --- a/src/Tools/Code/code_preproc.ML	Wed Jul 08 21:33:00 2015 +0200
     2.2 +++ b/src/Tools/Code/code_preproc.ML	Thu Jul 09 00:39:49 2015 +0200
     2.3 @@ -21,7 +21,7 @@
     2.4    val sortargs: code_graph -> string -> sort list
     2.5    val all: code_graph -> string list
     2.6    val pretty: Proof.context -> code_graph -> Pretty.T
     2.7 -  val obtain: bool -> theory -> string list -> term list -> code_algebra * code_graph
     2.8 +  val obtain: bool -> Proof.context -> string list -> term list -> code_algebra * code_graph
     2.9    val dynamic_conv: Proof.context
    2.10      -> (code_algebra -> code_graph -> term -> conv) -> conv
    2.11    val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'b)
    2.12 @@ -536,15 +536,15 @@
    2.13  
    2.14  (** retrieval and evaluation interfaces **)
    2.15  
    2.16 -fun obtain ignore_cache thy consts ts = apsnd snd
    2.17 -  (Wellsorted.change_yield (if ignore_cache then NONE else SOME thy)
    2.18 -    (extend_arities_eqngr (Proof_Context.init_global thy) consts ts));
    2.19 +fun obtain ignore_cache ctxt consts ts = apsnd snd
    2.20 +  (Wellsorted.change_yield (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
    2.21 +    (extend_arities_eqngr ctxt consts ts));
    2.22  
    2.23  fun dynamic_evaluator eval ctxt t =
    2.24    let
    2.25      val consts = fold_aterms
    2.26        (fn Const (c, _) => insert (op =) c | _ => I) t [];
    2.27 -    val (algebra, eqngr) = obtain false (Proof_Context.theory_of ctxt) consts [t];
    2.28 +    val (algebra, eqngr) = obtain false ctxt consts [t];
    2.29    in eval algebra eqngr t end;
    2.30  
    2.31  fun dynamic_conv ctxt conv =
    2.32 @@ -555,12 +555,12 @@
    2.33  
    2.34  fun static_conv { ctxt, consts } conv =
    2.35    let
    2.36 -    val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
    2.37 +    val (algebra, eqngr) = obtain true ctxt consts [];
    2.38    in Sandwich.conversion (value_sandwich ctxt) (conv { algebra = algebra, eqngr = eqngr }) end;
    2.39  
    2.40  fun static_value { ctxt, lift_postproc, consts } evaluator =
    2.41    let
    2.42 -    val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
    2.43 +    val (algebra, eqngr) = obtain true ctxt consts [];
    2.44    in Sandwich.evaluation (value_sandwich ctxt) lift_postproc (evaluator { algebra = algebra, eqngr = eqngr }) end;
    2.45  
    2.46  
     3.1 --- a/src/Tools/Code/code_thingol.ML	Wed Jul 08 21:33:00 2015 +0200
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Jul 09 00:39:49 2015 +0200
     3.3 @@ -790,7 +790,8 @@
     3.4      fun generate_consts ctxt algebra eqngr =
     3.5        fold_map (ensure_const ctxt algebra eqngr permissive);
     3.6    in
     3.7 -    invoke_generation permissive thy (Code_Preproc.obtain false thy consts [])
     3.8 +    invoke_generation permissive thy
     3.9 +      (Code_Preproc.obtain false (Proof_Context.init_global thy) consts [])
    3.10        generate_consts consts
    3.11      |> snd
    3.12    end;
    3.13 @@ -918,7 +919,7 @@
    3.14  
    3.15  fun code_depgr ctxt consts =
    3.16    let
    3.17 -    val (_, eqngr) = Code_Preproc.obtain true ((Proof_Context.theory_of ctxt)) consts [];
    3.18 +    val (_, eqngr) = Code_Preproc.obtain true ctxt consts [];
    3.19      val all_consts = Graph.all_succs eqngr consts;
    3.20    in Graph.restrict (member (op =) all_consts) eqngr end;
    3.21