src/Pure/library.ML

   val hd: 'a list -> 'a
   val tl: 'a list -> 'a list
   val cons: 'a -> 'a list -> 'a list
   val single: 'a -> 'a list
   val append: 'a list -> 'a list -> 'a list
+  val rev_append: 'a list -> 'a list -> 'a list
   val apply: ('a -> 'a) list -> 'a -> 'a
   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 foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list

 fun cons x xs = x :: xs;
 fun single x = [x];
 
 fun append xs ys = xs @ ys;
 
+(* tail recursive version *)
+fun rev_append [] ys = ys
+  | rev_append (x :: xs) ys = rev_append xs (x :: ys);
+
 fun apply [] x = x
   | apply (f :: fs) x = apply fs (f x);
 
 
 (* fold *)