# HG changeset patch
# User haftmann
# Date 1485443178 -3600
# Node ID de7ce0fad5bc4cae469e274ae429f557733139f5
# Parent  25281bee02ac0b8b7f69a4417f7cdffb2064e8c1
tuned scope of lazy computation

diff -r 25281bee02ac -r de7ce0fad5bc src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu Jan 26 16:06:18 2017 +0100
+++ b/src/Tools/Code/code_runtime.ML	Thu Jan 26 16:06:18 2017 +0100
@@ -418,8 +418,9 @@
 
 val is_first_occurrence = #first_occurrence o Code_Antiq_Data.get;
 
-fun lazy_code ctxt program consts = Lazy.lazy (fn () =>
+fun lazy_code ctxt consts = Lazy.lazy (fn () =>
   let
+    val program = Code_Thingol.consts_program ctxt consts;
     val (code, (_, consts_map)) =
       evaluation_code ctxt Code_Target.generatedN program [] consts
   in { code = code, consts_map = consts_map } end);
@@ -427,13 +428,12 @@
 fun register_const const ctxt =
   let
     val consts = insert (op =) const ((#named_consts o Code_Antiq_Data.get) ctxt);
-    val program = Code_Thingol.consts_program ctxt consts;
   in
     ctxt
     |> Code_Antiq_Data.put { 
         named_consts = consts,
         first_occurrence = false,
-        generated_code = lazy_code ctxt program consts
+        generated_code = lazy_code ctxt consts
       }
   end;