src/Pure/General/file.ML

   val standard_path: Path.T -> string
   val platform_path: Path.T -> string
   val bash_path: Path.T -> string
   val bash_paths: Path.T list -> string
   val bash_platform_path: Path.T -> string
+  val absolute_path: Path.T -> Path.T
   val full_path: Path.T -> Path.T -> Path.T
   val tmp_path: Path.T -> Path.T
   val exists: Path.T -> bool
   val rm: Path.T -> unit
   val is_dir: Path.T -> bool

 val bash_platform_path = Bash.string o platform_path;
 
 
 (* full_path *)
 
+val absolute_path =
+  Path.expand #> (fn path =>
+    if Path.is_absolute path then path
+    else Path.explode (ML_System.standard_path (OS.FileSys.getDir ())) + path);
+
 fun full_path dir path =
   let
     val path' = Path.expand path;
     val _ = Path.is_current path' andalso error "Bad file specification";
-    val path'' = dir + path';
-  in
-    if Path.is_absolute path'' then path''
-    else Path.explode (ML_System.standard_path (OS.FileSys.getDir ())) + path''
-  end;
+  in absolute_path (dir + path') end;
 
 
 (* tmp_path *)
 
 fun tmp_path path = Path.variable "ISABELLE_TMP" + Path.base path;