src/Pure/General/file.ML

--- a/src/Pure/General/file.ML	Mon Aug 23 16:41:06 2004 +0200
+++ b/src/Pure/General/file.ML	Mon Aug 23 17:06:18 2004 +0200
@@ -49,9 +49,17 @@
 val cd = Library.cd o sysify_path;
 val pwd = unsysify_path o Library.pwd;
 
-fun full_path path =
-  if Path.is_absolute path then path
-  else Path.append (pwd ()) path;
+fun norm_absolute p =
+  let
+    val p' = pwd ();
+    fun norm p = if can cd p then pwd ()
+      else Path.append (norm (Path.dir p)) (Path.base p);
+    val p'' = norm p
+  in (cd p'; p'') end
+
+fun full_path path = norm_absolute
+  (if Path.is_absolute path then path
+   else Path.append (pwd ()) path);
 
 
 (* tmp_path *)