# HG changeset patch
# User wenzelm
# Date 754654077 -3600
# Node ID 3224c46737ef2daae6be3069a3c180914da1df62
# Parent  ab0f93a291b54821ac53b373f07e1f79ab4427ba
changed split_filename, remove_ext;
added base_name;

diff -r ab0f93a291b5 -r 3224c46737ef src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Nov 30 11:04:07 1993 +0100
+++ b/src/Pure/library.ML	Tue Nov 30 11:07:57 1993 +0100
@@ -624,9 +624,10 @@
 
 (*Convert Unix filename of the form path/file to "path/" and "file" ;
   if filename contains no slash, then it returns "" and "file" *)
-fun split_filename name =
-  let val (file,path) = take_prefix (apr(op<>,"/")) (rev (explode name))
-  in  (implode(rev path), implode(rev file)) end;
+val split_filename =
+  (pairself implode) o take_suffix (not_equal "/") o explode;
+
+val base_name = #2 o split_filename;
 
 (*Merge splitted filename (path and file);
   if path does not end with one a slash is appended *)
@@ -636,7 +637,4 @@
       else path ^ "/" ^ name;
 
 (*Remove the extension of a filename, i.e. the part after the last '.' *)
-fun remove_ext name =
-  let val (file,_) = take_prefix (apr(op<>,".")) (rev (explode name))
-  in implode (rev file) end;
-
+val remove_ext = implode o #1 o take_suffix (not_equal ".") o explode;