diff -r a471730347e0 -r 460d743010bc src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Tools/Code/code_target.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -304,7 +304,7 @@
       Singleton (ext, p) => export (binding (Path.ext ext prefix)) (format p)
     | Hierarchy modules =>
         fold (fn (names, p) =>
-          export (binding (Path.append prefix (Path.make names))) (format p)) modules)
+          export (binding (prefix + Path.make names)) (format p)) modules)
     #> tap code_export_message
   end;