# HG changeset patch
# User wenzelm
# Date 1345580794 -7200
# Node ID 51659a3819a74c784eabdcf7d2a5bc691c05ac52
# Parent  157dd47032e0060272ee2e6a4e53283d738ac9fb
prefer File.full_path in accordance to check_file;

diff -r 157dd47032e0 -r 51659a3819a7 src/Pure/Thy/thy_load.ML
--- 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 =