tuned;
authorwenzelm
Sat, 27 Nov 2010 15:36:35 +0100
changeset 409970e7c2957fc1d
parent 40996 b07a0dbc8a38
child 40998 1dabcda202c3
tuned;
src/Pure/General/file.ML
     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