refined semantics of mkdir_leaf: do not fail if directory already exists

--- a/src/Pure/General/file.ML	Thu Jul 01 13:32:14 2010 +0200
+++ b/src/Pure/General/file.ML	Thu Jul 01 13:38:17 2010 +0200
@@ -136,7 +136,7 @@
 
 fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
 
-fun mkdir_leaf path = system_command ("mkdir " ^ shell_path path);
+fun mkdir_leaf path = (check (Path.dir path); mkdir path);
 
 fun is_dir path =
   the_default false (try OS.FileSys.isDir (platform_path path));