--- a/src/Pure/General/path.ML Thu Jun 01 21:24:33 2017 +0200
+++ b/src/Pure/General/path.ML Thu Jun 01 21:43:36 2017 +0200
@@ -29,6 +29,7 @@
val print: T -> string
val dir: T -> T
val base: T -> T
+ val base_name: T -> string
val ext: string -> T -> T
val split_ext: T -> T * string
val expand: T -> T
@@ -183,6 +184,7 @@
val dir = split_path #1;
val base = split_path (fn (_, s) => Path [Basic s]);
+val base_name = implode_path o base;
fun ext "" = I
| ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));