# HG changeset patch
# User wenzelm
# Date 1314997452 -7200
# Node ID 178a6f0ed29d8b8c5800392b68afce27dc8b8947
# Parent  f64c715660c3ba4f1b3dfaedbb0df2ab533797cb# Parent  c8f1d943bfc5fbddb0bcb45a6a4df961d123bcd8
merged

diff -r c8f1d943bfc5 -r 178a6f0ed29d src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Sep 02 22:48:56 2011 +0200
+++ b/src/Tools/Code/code_runtime.ML	Fri Sep 02 23:04:12 2011 +0200
@@ -47,6 +47,7 @@
 val s_Holds = Long_Name.append this "Holds";
 
 val target = "Eval";
+val structure_generated = "Generated_Code";
 
 datatype truth = Holds;
 
@@ -227,7 +228,7 @@
     val tycos' = fold (insert (op =)) new_tycos tycos;
     val consts' = fold (insert (op =)) new_consts consts;
     val acc_code = Lazy.lazy (fn () =>
-      evaluation_code (Proof_Context.theory_of ctxt) "Code" tycos' consts'
+      evaluation_code (Proof_Context.theory_of ctxt) structure_generated tycos' consts'
       |> apsnd snd);
   in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
 
@@ -434,7 +435,7 @@
   |-> (fn ([Const (const, _)], _) =>
      Code_Target.add_const_syntax target const
        (SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))
-  #> tap (fn thy => Code_Target.produce_code thy [const] target NONE "Code" []));
+  #> tap (fn thy => Code_Target.produce_code thy [const] target NONE structure_generated []));
 
 fun process_file filepath (definienda, thy) =
   let