src/Pure/General/path.ML

       else if x = Root then rev_app (x :: xs) ys
       else rev_app xs ys
   | rev_app xs (y :: ys) = rev_app (y :: xs) ys;
 
 fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
-fun appends paths = foldl (uncurry append) (current, paths);
+fun appends paths = Library.foldl (uncurry append) (current, paths);
 val make = appends o map basic;
 fun norm path = rev_app [] path;
 
 
 (* pack *)

   | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path;
 
 val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
   (case take_suffix (not_equal ".") (explode s) of
     ([], _) => (Path [Basic s], "")
-  | (cs, e) => (Path [Basic (implode (take (length cs - 1, cs)))], implode e)));
+  | (cs, e) => (Path [Basic (implode (Library.take (length cs - 1, cs)))], implode e)));
 
 
 (* evaluate variables *)
 
 fun eval env (Variable s) = rep (env s)
   | eval _ x = [x];
 
 fun evaluate env (Path xs) =
-  Path (norm (flat (map (eval env) xs)));
+  Path (norm (List.concat (map (eval env) xs)));
 
 val expand = evaluate (unpack o getenv);
 
 val position = Position.line_name 1 o quote o pack o expand;