src/Tools/Code/code_runtime.ML
changeset 44663 3bc39cfe27fe
parent 43619 3803869014aa
child 45268 a42624e9de09
     1.1 --- a/src/Tools/Code/code_runtime.ML	Fri Sep 02 18:17:45 2011 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Sep 02 19:29:36 2011 +0200
     1.3 @@ -47,6 +47,7 @@
     1.4  val s_Holds = Long_Name.append this "Holds";
     1.5  
     1.6  val target = "Eval";
     1.7 +val structure_generated = "Generated_Code";
     1.8  
     1.9  datatype truth = Holds;
    1.10  
    1.11 @@ -227,7 +228,7 @@
    1.12      val tycos' = fold (insert (op =)) new_tycos tycos;
    1.13      val consts' = fold (insert (op =)) new_consts consts;
    1.14      val acc_code = Lazy.lazy (fn () =>
    1.15 -      evaluation_code (Proof_Context.theory_of ctxt) "Code" tycos' consts'
    1.16 +      evaluation_code (Proof_Context.theory_of ctxt) structure_generated tycos' consts'
    1.17        |> apsnd snd);
    1.18    in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
    1.19  
    1.20 @@ -434,7 +435,7 @@
    1.21    |-> (fn ([Const (const, _)], _) =>
    1.22       Code_Target.add_const_syntax target const
    1.23         (SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))
    1.24 -  #> tap (fn thy => Code_Target.produce_code thy [const] target NONE "Code" []));
    1.25 +  #> tap (fn thy => Code_Target.produce_code thy [const] target NONE structure_generated []));
    1.26  
    1.27  fun process_file filepath (definienda, thy) =
    1.28    let