src/Pure/Thy/thy_info.ML

 local
 
 fun provide path name info (deps as SOME {present, outdated, master, files}) =
      (if exists (equal path o #1) files then ()
       else warning (loader_msg "undeclared dependency of theory" [name] ^
-        " on file: " ^ quote (Path.pack path));
+        " on file: " ^ quote (Path.implode path));
       SOME (make_deps present outdated master (AList.update (op =) (path, SOME info) files)))
   | provide _ _ _ NONE = NONE;
 
 fun run_file path =
   (case Option.map Context.theory_name (Context.get_context ()) of

 
 in
 
 fun load_file time path = Output.toplevel_errors (fn () =>
   if time then
-    let val name = Path.pack path in
+    let val name = Path.implode path in
       timeit (fn () =>
        (priority ("\n**** Starting file " ^ quote name ^ " ****");
         run_file path;
         priority ("**** Finished file " ^ quote name ^ " ****\n")))
     end
   else run_file path) ();
 
-val use = load_file false o Path.unpack;
-val time_use = load_file true o Path.unpack;
+val use = load_file false o Path.explode;
+val time_use = load_file true o Path.explode;
 
 end;
 
 
 (* load_thy *)

     val master =
       if really then ThyLoad.load_thy dir name ml time
       else #1 (ThyLoad.deps_thy dir name ml);
 
     val files = get_files name;
-    val missing_files = map_filter (fn (path, NONE) => SOME (Path.pack path) | _ => NONE) files;
+    val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files;
   in
     if null missing_files then ()
     else warning (loader_msg "unresolved dependencies of theory" [name] ^
       " on file(s): " ^ commas_quote missing_files);
     change_deps name (fn _ => SOME (make_deps true false (SOME master) files));

   end;
 
 
 (* require_thy *)
 
-fun base_of_path s = Path.pack (Path.base (Path.unpack s));
+fun base_of_path s = Path.implode (Path.base (Path.explode s));
 
 local
 
 fun load_deps ml dir name =
   let val (master, (parents, files)) = ThyLoad.deps_thy dir name ml

   (case lookup_deps name of
     NONE => (false, load_deps ml dir name)
   | SOME deps =>
       let
         fun get_name s = (case opt_path'' (lookup_deps s) of NONE => s
-          | SOME p => Path.pack (Path.append p (Path.basic s)));
+          | SOME p => Path.implode (Path.append p (Path.basic s)));
         val same_deps = (NONE, map get_name (thy_graph Graph.imm_preds name))
       in
         (case deps of
           NONE => (true, same_deps)
         | SOME {present, outdated, master, files} =>

               end)
       end);
 
 fun require_thy really ml time strict keep_strict initiators prfx (visited, str) =
   let
-    val path = Path.expand (Path.unpack str);
-    val name = Path.pack (Path.base path);
+    val path = Path.expand (Path.explode str);
+    val name = Path.implode (Path.base path);
   in
     if member (op =) initiators name then error (cycle_msg initiators) else ();
     if known_thy name andalso is_finished name orelse member (op =) visited name then
       (visited, (true, name))
     else

 
 fun check_uses name uses =
   let val illegal = map (fn ext => Path.ext ext (Path.basic name)) ThyLoad.ml_exts in
     (case find_first (member (op =) illegal o Path.base o Path.expand o #1) uses of
       NONE => ()
-    | SOME (path, _) => error ("Illegal use of theory ML file: " ^ quote (Path.pack path)))
+    | SOME (path, _) => error ("Illegal use of theory ML file: " ^ quote (Path.implode path)))
   end;
 
 fun begin_theory present name parents uses int =
   let
     val bparents = map base_of_path parents;