diff -r 8d34e64eeaf6 -r 279b129498b6 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/General/file.ML	Sat Dec 30 16:08:00 2006 +0100
@@ -137,12 +137,15 @@
     SOME ids => OS.FileSys.compare ids = EQUAL
   | NONE => false);
 
-fun copy src dst = conditional (not (eq (src, dst))) (fn () =>
-  let val target = if is_dir dst then Path.append dst (Path.base src) else dst
-  in write target (read src) end);
+fun copy src dst =
+  if eq (src, dst) then ()
+  else
+    let val target = if is_dir dst then Path.append dst (Path.base src) else dst
+    in write target (read src) end;
 
-fun copy_dir src dst = conditional (not (eq (src, dst))) (fn () =>
-  (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ()))
+fun copy_dir src dst =
+  if eq (src, dst) then ()
+  else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ());
 
 
 (* use ML files *)