# HG changeset patch
# User haftmann
# Date 1314984588 -7200
# Node ID f64c715660c3ba4f1b3dfaedbb0df2ab533797cb
# Parent  17dbd9d9db380a47fe94a108036fac7ce1216a3e# Parent  3bc39cfe27fee166cab5a239a1a25931aa7c9027
merged

diff -r 17dbd9d9db38 -r f64c715660c3 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Sep 02 19:25:44 2011 +0200
+++ b/src/Tools/Code/code_runtime.ML	Fri Sep 02 19:29:48 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