src/Tools/Code/code_runtime.ML
changeset 40422 d425d1ed82af
parent 40421 b41aabb629ce
child 40711 81bc73585eec
     1.1 --- a/src/Tools/Code/code_runtime.ML	Mon Nov 08 10:43:24 2010 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Nov 08 10:56:48 2010 +0100
     1.3 @@ -226,7 +226,7 @@
     1.4      val consts' = fold (insert (op =)) new_consts consts;
     1.5      val acc_code = Lazy.lazy (fn () =>
     1.6        evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts'
     1.7 -      |> apsnd fst);
     1.8 +      |> apsnd snd);
     1.9    in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
    1.10  
    1.11  fun register_const const = register_code [] [const];
    1.12 @@ -238,8 +238,7 @@
    1.13    let
    1.14      val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
    1.15      val (ml_code, consts_map) = Lazy.force acc_code;
    1.16 -    val ml_code = if is_first then ml_code
    1.17 -      else "";
    1.18 +    val ml_code = if is_first then ml_code else "";
    1.19      val all_struct_name = "Isabelle";
    1.20    in (ml_code, print_const const all_struct_name consts_map) end;
    1.21