more permissive Isabelle_System.mkdir;
exported File.is_dir (weak test);

--- a/src/Pure/General/file.ML	Sun Nov 28 16:15:31 2010 +0100
+++ b/src/Pure/General/file.ML	Sun Nov 28 16:35:56 2010 +0100
@@ -16,6 +16,7 @@
   val exists: Path.T -> bool
   val check: Path.T -> unit
   val rm: Path.T -> unit
+  val is_dir: Path.T -> bool
   val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
   val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
   val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
@@ -71,6 +72,9 @@
 
 val rm = OS.FileSys.remove o platform_path;
 
+fun is_dir path =
+  the_default false (try OS.FileSys.isDir (platform_path path));
+
 
 (* open files *)
 
@@ -128,9 +132,6 @@
     SOME ids => is_equal (OS.FileSys.compare ids)
   | NONE => false);
 
-fun is_dir path =
-  the_default false (try OS.FileSys.isDir (platform_path path));
-
 fun copy src dst =
   if eq (src, dst) then ()
   else

--- a/src/Pure/System/isabelle_system.ML	Sun Nov 28 16:15:31 2010 +0100
+++ b/src/Pure/System/isabelle_system.ML	Sun Nov 28 16:35:56 2010 +0100
@@ -41,7 +41,8 @@
 
 fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
 
-val mkdir = OS.FileSys.mkDir o File.platform_path;
+fun mkdir path =
+  if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
 
 fun copy_dir src dst =
   if File.eq (src, dst) then ()