--- a/src/Tools/Code/code_runtime.ML Wed Feb 29 17:43:41 2012 +0100
+++ b/src/Tools/Code/code_runtime.ML Wed Feb 29 23:09:06 2012 +0100
@@ -310,8 +310,9 @@
| process_reflection (code, _) _ (SOME file_name) thy =
let
val preamble =
- "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
- ^ "; DO NOT EDIT! *)";
+ "(* Generated from " ^
+ Path.implode (Thy_Load.thy_path (Path.basic (Context.theory_name thy))) ^
+ "; DO NOT EDIT! *)";
val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code);
in
thy