author | wenzelm |
Tue, 21 Aug 2012 22:26:34 +0200 | |
changeset 48877 | 51659a3819a7 |
parent 48876 | 157dd47032e0 |
child 48878 | 5e850e6fa3c3 |
--- a/src/Pure/Thy/thy_load.ML Tue Aug 21 21:48:32 2012 +0200 +++ b/src/Pure/Thy/thy_load.ML Tue Aug 21 22:26:34 2012 +0200 @@ -121,7 +121,7 @@ val path = Path.explode (Token.content_of tok); val files = command_files path (Keyword.command_files cmd) - |> map (Path.append dir #> (fn path => (File.read path, Path.position path))); + |> map (File.full_path dir #> (fn path => (File.read path, Path.position path))); in (dir, files) end; fun parse_files cmd =