Added function rev_append.

--- a/src/Pure/library.ML	Wed Jan 29 17:32:01 2003 +0100
+++ b/src/Pure/library.ML	Wed Jan 29 17:32:19 2003 +0100
@@ -81,6 +81,7 @@
   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
@@ -453,6 +454,10 @@
 
 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);