diff -r dbb48b0744d3 -r c905fe5994a2 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Thu Feb 11 15:30:10 1999 +0100
+++ b/src/Pure/General/path.ML	Thu Feb 11 21:15:27 1999 +0100
@@ -18,6 +18,7 @@
   val is_absolute: T -> bool
   val is_basic: T -> bool
   val append: T -> T -> T
+  val appends: T list -> T
   val pack: T -> string
   val unpack: string -> T
   val base: T -> T
@@ -80,6 +81,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 norm path = rev_app [] path;