--- a/src/Pure/Tools/generated_files.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/Tools/generated_files.ML Tue Oct 27 22:34:37 2020 +0100
@@ -146,7 +146,7 @@
fun write_file dir (file: file) =
let
- val path = Path.expand (Path.append dir (#path file));
+ val path = Path.expand (dir + #path file);
val _ = Isabelle_System.make_directory (Path.dir path);
val _ = File.generate path (#content file);
in () end;
@@ -298,7 +298,7 @@
val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe);
val (path, pos) = Path.dest_binding binding;
val content =
- (case try File.read (Path.append dir path) of
+ (case try File.read (dir + path) of
SOME context => context
| NONE => error ("Missing result file " ^ Path.print path ^ Position.here pos));
val _ = Export.report_export thy export_prefix;