diff -r 177e8cea3e09 -r c755df0f7062 src/Pure/General/file.ML
--- 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