src/Pure/General/path.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 17827 b32fad049413
     1.1 --- a/src/Pure/General/path.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/General/path.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -90,7 +90,7 @@
     1.4    | rev_app xs (y :: ys) = rev_app (y :: xs) ys;
     1.5  
     1.6  fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
     1.7 -fun appends paths = foldl (uncurry append) (current, paths);
     1.8 +fun appends paths = Library.foldl (uncurry append) (current, paths);
     1.9  val make = appends o map basic;
    1.10  fun norm path = rev_app [] path;
    1.11  
    1.12 @@ -142,7 +142,7 @@
    1.13  val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
    1.14    (case take_suffix (not_equal ".") (explode s) of
    1.15      ([], _) => (Path [Basic s], "")
    1.16 -  | (cs, e) => (Path [Basic (implode (take (length cs - 1, cs)))], implode e)));
    1.17 +  | (cs, e) => (Path [Basic (implode (Library.take (length cs - 1, cs)))], implode e)));
    1.18  
    1.19  
    1.20  (* evaluate variables *)
    1.21 @@ -151,7 +151,7 @@
    1.22    | eval _ x = [x];
    1.23  
    1.24  fun evaluate env (Path xs) =
    1.25 -  Path (norm (flat (map (eval env) xs)));
    1.26 +  Path (norm (List.concat (map (eval env) xs)));
    1.27  
    1.28  val expand = evaluate (unpack o getenv);
    1.29