--- a/src/Pure/General/path.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/src/Pure/General/path.ML Thu Mar 03 12:43:01 2005 +0100
@@ -90,7 +90,7 @@
| 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;
@@ -142,7 +142,7 @@
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 *)
@@ -151,7 +151,7 @@
| 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);