# HG changeset patch
# User haftmann
# Date 1314984576 -7200
# Node ID 3bc39cfe27fee166cab5a239a1a25931aa7c9027
# Parent  fe03653315667519fd9f54b81451a6e81a307e53
avoid "Code" as structure name

diff -r fe0365331566 -r 3bc39cfe27fe src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Sep 02 18:17:45 2011 +0200
+++ b/src/Tools/Code/code_runtime.ML	Fri Sep 02 19:29:36 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