src/Pure/General/file.ML

--- a/src/Pure/General/file.ML	Sat Feb 27 16:33:16 2021 +0100
+++ b/src/Pure/General/file.ML	Sat Feb 27 17:25:54 2021 +0100
@@ -11,6 +11,7 @@
   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
@@ -56,15 +57,16 @@
 
 (* 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 *)