src/Pure/library.ML

   exception LIST of string
   val null: 'a list -> bool
   val hd: 'a list -> 'a
   val tl: 'a list -> 'a list
   val cons: 'a -> 'a list -> 'a list
+  val append: 'a list -> 'a list -> 'a list
   val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
   val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
   val length: 'a list -> int
   val take: int * 'a list -> 'a list

 fun tl [] = raise LIST "tl"
   | tl (_ :: xs) = xs;
 
 fun cons x xs = x :: xs;
 
+fun append xs ys = xs @ ys;
+
 
 (* fold *)
 
 (*the following versions of fold are designed to fit nicely with infixes*)