# HG changeset patch
# User haftmann
# Date 1412533856 -7200
# Node ID fea97f7be494ece08d2200dd3e974e79c978fc12
# Parent  71a63f8a5b845afe9531bb161e72303caf3be53e
split dynamic from static context

diff -r 71a63f8a5b84 -r fea97f7be494 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Sun Oct 05 23:09:27 2014 +0200
+++ b/src/Tools/Code/code_runtime.ML	Sun Oct 05 20:30:56 2014 +0200
@@ -196,10 +196,9 @@
 
 (** instrumentalization **)
 
-fun evaluation_code ctxt module_name tycos consts =
+fun evaluation_code ctxt module_name program tycos consts =
   let
     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 ctxt
         target NONE module_name [] program false (map Constant consts @ map Type_Constructor tycos);
@@ -236,8 +235,9 @@
     val ((tycos, consts), _) = Code_Antiq_Data.get ctxt;
     val tycos' = fold (insert (op =)) new_tycos tycos;
     val consts' = fold (insert (op =)) new_consts consts;
+    val program = Code_Thingol.consts_program (Proof_Context.theory_of ctxt) consts';
     val acc_code = Lazy.lazy (fn () =>
-      evaluation_code ctxt structure_generated tycos' consts'
+      evaluation_code ctxt structure_generated program tycos' consts'
       |> apsnd snd);
   in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
 
@@ -336,7 +336,9 @@
     val (tycos, constrs) = map_split (uncurry (check_datatype thy)) datatypes
       |> apsnd flat;
     val functions = map (prep_const thy) raw_functions;
-    val result = evaluation_code ctxt module_name tycos (constrs @ functions)
+    val consts = constrs @ functions;
+    val program = Code_Thingol.consts_program (Proof_Context.theory_of ctxt) consts;
+    val result = evaluation_code ctxt module_name program tycos consts
       |> (apsnd o apsnd) (chop (length constrs));
   in
     thy