val appends: T list -> T;
authorwenzelm
Thu Feb 11 21:15:27 1999 +0100 (1999-02-11)
changeset 6270c905fe5994a2
parent 6269 dbb48b0744d3
child 6271 957d8aa4a06b
val appends: T list -> T;
src/Pure/General/path.ML
     1.1 --- a/src/Pure/General/path.ML	Thu Feb 11 15:30:10 1999 +0100
     1.2 +++ b/src/Pure/General/path.ML	Thu Feb 11 21:15:27 1999 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4    val is_absolute: T -> bool
     1.5    val is_basic: T -> bool
     1.6    val append: T -> T -> T
     1.7 +  val appends: T list -> T
     1.8    val pack: T -> string
     1.9    val unpack: string -> T
    1.10    val base: T -> T
    1.11 @@ -80,6 +81,7 @@
    1.12    | rev_app xs (y :: ys) = rev_app (y :: xs) ys;
    1.13  
    1.14  fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
    1.15 +fun appends paths = foldl (uncurry append) (current, paths);
    1.16  fun norm path = rev_app [] path;
    1.17  
    1.18