src/Pure/Tools/generated_files.ML
changeset 69784 24bbc4e30e5b
parent 69662 fd86ed39aea4
child 70012 36aeb535a801
     1.1 --- a/src/Pure/Tools/generated_files.ML	Sat Feb 02 14:51:11 2019 +0100
     1.2 +++ b/src/Pure/Tools/generated_files.ML	Sat Feb 02 15:52:14 2019 +0100
     1.3 @@ -81,7 +81,7 @@
     1.4  fun export_files thy other_thys =
     1.5    other_thys |> maps (fn other_thy =>
     1.6      get_files other_thy |> map (fn {path, pos, text} =>
     1.7 -      (Export.export thy (Path.implode path) [text]; (path, pos))));
     1.8 +      (Export.export thy path [text]; (path, pos))));
     1.9  
    1.10  
    1.11  (* file types *)