--- 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