diff -r f9d085c2625c -r 05f57309170c src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/file.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -7,8 +7,8 @@
 
 signature FILE =
 sig
-  val unpack_platform_path_fn: (string -> Path.T) ref
-  val unpack_platform_path: string -> Path.T
+  val explode_platform_path_fn: (string -> Path.T) ref
+  val explode_platform_path: string -> Path.T
   val platform_path_fn: (Path.T -> string) ref
   val platform_path: Path.T -> string
   val shell_path_fn: (Path.T -> string) ref
@@ -22,7 +22,7 @@
   eqtype info
   val info: Path.T -> info option
   val exists: Path.T -> bool
-  val assert: Path.T -> unit
+  val check: Path.T -> unit
   val rm: Path.T -> unit
   val mkdir: Path.T -> unit
   val read: Path.T -> string
@@ -41,20 +41,20 @@
 
 (* platform specific path representations *)
 
-val unpack_platform_path_fn = ref Path.unpack;
-fun unpack_platform_path s = ! unpack_platform_path_fn s;
+val explode_platform_path_fn = ref Path.explode;
+fun explode_platform_path s = ! explode_platform_path_fn s;
 
-val platform_path_fn = ref (Path.pack o Path.expand);
+val platform_path_fn = ref (Path.implode o Path.expand);
 fun platform_path path = ! platform_path_fn path;
 
-val shell_path_fn = ref (enclose "'" "'" o Path.pack o Path.expand);
+val shell_path_fn = ref (enclose "'" "'" o Path.implode o Path.expand);
 fun shell_path path = ! shell_path_fn path;
 
 
 (* current path *)
 
 val cd = Library.cd o platform_path;
-val pwd = unpack_platform_path o Library.pwd;
+val pwd = explode_platform_path o Library.pwd;
 
 fun norm_absolute p =
   let
@@ -94,9 +94,9 @@
 
 val exists = is_some o info;
 
-fun assert path =
+fun check path =
   if exists path then ()
-  else error ("No such file or directory: " ^ quote (Path.pack path));
+  else error ("No such file or directory: " ^ quote (Path.implode path));
 
 val rm = OS.FileSys.remove o platform_path;
 
@@ -137,12 +137,12 @@
     SOME ids => OS.FileSys.compare ids = EQUAL
   | NONE => false);
 
-fun copy from to = conditional (not (eq (from, to))) (fn () =>
-  let val target = if is_dir to then Path.append to (Path.base from) else to
-  in write target (read from) end);
+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_dir from to = conditional (not (eq (from, to))) (fn () =>
-  (system_command ("cp -r -f " ^ shell_path from ^ "/. " ^ shell_path to); ()))
+fun copy_dir src dst = conditional (not (eq (src, dst))) (fn () =>
+  (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ()))
 
 
 (* use ML files *)