src/Tools/Code/code_runtime.ML
changeset 63159 84c6dd947b75
parent 63157 65a81a4ef7f8
child 63160 80a91e0e236e
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
     1.3 @@ -338,7 +338,7 @@
     1.4      val ((tycos, consts), _) = Code_Antiq_Data.get ctxt;
     1.5      val tycos' = fold (insert (op =)) new_tycos tycos;
     1.6      val consts' = fold (insert (op =)) new_consts consts;
     1.7 -    val program = Code_Thingol.consts_program (Proof_Context.theory_of ctxt) consts';
     1.8 +    val program = Code_Thingol.consts_program ctxt consts';
     1.9      val acc_code = Lazy.lazy (fn () =>
    1.10        evaluation_code ctxt structure_generated program tycos' consts'
    1.11        |> apsnd snd);
    1.12 @@ -440,7 +440,7 @@
    1.13        |> apsnd flat;
    1.14      val functions = map (prep_const thy) raw_functions;
    1.15      val consts = constrs @ functions;
    1.16 -    val program = Code_Thingol.consts_program (Proof_Context.theory_of ctxt) consts;
    1.17 +    val program = Code_Thingol.consts_program ctxt consts;
    1.18      val result = evaluation_code ctxt module_name program tycos consts
    1.19        |> (apsnd o apsnd) (chop (length constrs));
    1.20    in