src/Tools/Code/code_target.ML

   in mounted_serializer prepared_program end;
 
 fun assert_module_name "" = error ("Empty module name not allowed.")
   | assert_module_name module_name = module_name;
 
+fun using_master_directory thy = Option.map (Path.append (Thy_Load.master_directory thy));
+
 in
 
 fun export_code_for thy some_path target some_width module_name args =
-  export some_path ooo invoke_serializer thy target some_width module_name args;
+  export (using_master_directory thy some_path)
+  ooo invoke_serializer thy target some_width module_name args;
 
 fun produce_code_for thy target some_width module_name args =
   let
     val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
   in fn naming => fn program => fn names =>