src/Tools/Code/code_runtime.ML

 val this = "Code_Runtime";
 val s_truth = Long_Name.append this "truth";
 val s_Holds = Long_Name.append this "Holds";
 
 val target = "Eval";
+val structure_generated = "Generated_Code";
 
 datatype truth = Holds;
 
 val _ = Context.>> (Context.map_theory
   (Code_Target.extend_target (target, (Code_ML.target_SML, K I))

   let
     val ((tycos, consts), _) = Code_Antiq_Data.get ctxt;
     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;
 
 fun register_const const = register_code [] [const];
 

   |> Code_Target.add_reserved target ml_name
   |> Specification.axiomatization [(b, SOME T, NoSyn)] []
   |-> (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
     val (ml_names, thy') = use_file filepath thy;
     val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names;