src/Tools/Code/code_target.ML
changeset 69784 24bbc4e30e5b
parent 69698 1a249d1c884b
child 69906 55534affe445
     1.1 --- a/src/Tools/Code/code_target.ML	Sat Feb 02 14:51:11 2019 +0100
     1.2 +++ b/src/Tools/Code/code_target.ML	Sat Feb 02 15:52:14 2019 +0100
     1.3 @@ -180,9 +180,10 @@
     1.4    (Export.export thy name [content]; writeln (Export.message thy ""));
     1.5  
     1.6  fun export_to_exports thy width (Singleton (extension, p)) =
     1.7 -      export_information thy (generatedN ^ "." ^ extension) (Code_Printer.format [] width p)
     1.8 +      export_information thy (Path.basic (generatedN ^ "." ^ extension))
     1.9 +        (Code_Printer.format [] width p)
    1.10    | export_to_exports thy width (Hierarchy code_modules) = (
    1.11 -      map (fn (names, p) => export_information thy (Path.implode (Path.make names))
    1.12 +      map (fn (names, p) => export_information thy (Path.make names)
    1.13          (Code_Printer.format [] width p)) code_modules;
    1.14        ());
    1.15