1.1 --- a/src/Pure/General/file.ML Sat Nov 27 15:28:00 2010 +0100
1.2 +++ b/src/Pure/General/file.ML Sat Nov 27 15:36:35 2010 +0100
1.3 @@ -67,9 +67,6 @@
1.4
1.5 val rm = OS.FileSys.remove o platform_path;
1.6
1.7 -fun is_dir path =
1.8 - the_default false (try OS.FileSys.isDir (platform_path path));
1.9 -
1.10
1.11 (* open files *)
1.12
1.13 @@ -127,6 +124,9 @@
1.14 SOME ids => is_equal (OS.FileSys.compare ids)
1.15 | NONE => false);
1.16
1.17 +fun is_dir path =
1.18 + the_default false (try OS.FileSys.isDir (platform_path path));
1.19 +
1.20 fun copy src dst =
1.21 if eq (src, dst) then ()
1.22 else