src/Tools/Code/code_runtime.ML
changeset 64954 e5f535f90d61
parent 64946 03b5f4e7f4a6
child 64955 25281bee02ac
     1.1 --- a/src/Tools/Code/code_runtime.ML	Fri Jan 27 17:35:08 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Jan 26 16:06:18 2017 +0100
     1.3 @@ -407,18 +407,16 @@
     1.4  
     1.5  val is_first_occ = fst o snd o Code_Antiq_Data.get;
     1.6  
     1.7 -fun register_code new_consts ctxt =
     1.8 +fun register_const const ctxt =
     1.9    let
    1.10      val (consts, _) = Code_Antiq_Data.get ctxt;
    1.11 -    val consts' = fold (insert (op =)) new_consts consts;
    1.12 +    val consts' = insert (op =) const consts;
    1.13      val program = Code_Thingol.consts_program ctxt consts';
    1.14      val acc_code = Lazy.lazy (fn () =>
    1.15        evaluation_code ctxt Code_Target.generatedN program [] consts'
    1.16        |> apsnd snd);
    1.17    in Code_Antiq_Data.put (consts', (false, acc_code)) ctxt end;
    1.18  
    1.19 -fun register_const const = register_code [const];
    1.20 -
    1.21  fun print_code is_first const ctxt =
    1.22    let
    1.23      val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;