src/Tools/Code/code_runtime.ML
changeset 64956 de7ce0fad5bc
parent 64955 25281bee02ac
child 64957 3faa9b31ff78
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu Jan 26 16:06:18 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Jan 26 16:06:18 2017 +0100
     1.3 @@ -418,8 +418,9 @@
     1.4  
     1.5  val is_first_occurrence = #first_occurrence o Code_Antiq_Data.get;
     1.6  
     1.7 -fun lazy_code ctxt program consts = Lazy.lazy (fn () =>
     1.8 +fun lazy_code ctxt consts = Lazy.lazy (fn () =>
     1.9    let
    1.10 +    val program = Code_Thingol.consts_program ctxt consts;
    1.11      val (code, (_, consts_map)) =
    1.12        evaluation_code ctxt Code_Target.generatedN program [] consts
    1.13    in { code = code, consts_map = consts_map } end);
    1.14 @@ -427,13 +428,12 @@
    1.15  fun register_const const ctxt =
    1.16    let
    1.17      val consts = insert (op =) const ((#named_consts o Code_Antiq_Data.get) ctxt);
    1.18 -    val program = Code_Thingol.consts_program ctxt consts;
    1.19    in
    1.20      ctxt
    1.21      |> Code_Antiq_Data.put { 
    1.22          named_consts = consts,
    1.23          first_occurrence = false,
    1.24 -        generated_code = lazy_code ctxt program consts
    1.25 +        generated_code = lazy_code ctxt consts
    1.26        }
    1.27    end;
    1.28