src/Pure/Tools/generated_files.ML

--- a/src/Pure/Tools/generated_files.ML	Sat Feb 02 14:51:11 2019 +0100
+++ b/src/Pure/Tools/generated_files.ML	Sat Feb 02 15:52:14 2019 +0100
@@ -81,7 +81,7 @@
 fun export_files thy other_thys =
   other_thys |> maps (fn other_thy =>
     get_files other_thy |> map (fn {path, pos, text} =>
-      (Export.export thy (Path.implode path) [text]; (path, pos))));
+      (Export.export thy path [text]; (path, pos))));
 
 
 (* file types *)