diff -r 4dc7ddb47350 -r 09ab89658a5d src/Tools/Code/code_runtime.ML --- 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