# HG changeset patch
# User webertj
# Date 1152980267 -7200
# Node ID 9ee091573fa038f51e700b5b193120d4f4bbcf26
# Parent  de3c295000b2ef638846bd05443b0fc7cc832122
function butlast added

diff -r de3c295000b2 -r 9ee091573fa0 src/Pure/library.ML
--- a/src/Pure/library.ML	Sat Jul 15 15:26:50 2006 +0200
+++ b/src/Pure/library.ML	Sat Jul 15 18:17:47 2006 +0200
@@ -103,6 +103,7 @@
   val cons: 'a -> 'a list -> 'a list
   val single: 'a -> 'a list
   val singleton: ('a list -> 'b list) -> 'a -> 'b
+  val butlast: 'a list -> 'a list
   val append: 'a list -> 'a list -> 'a list
   val apply: ('a -> 'a) list -> 'a -> 'a
   val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
@@ -496,6 +497,10 @@
 
 fun singleton f x = (case f [x] of [y] => y | _ => raise Empty);
 
+fun butlast []        = raise Empty
+  | butlast (x :: []) = []
+  | butlast (x :: xs) = x :: butlast xs;
+
 fun append xs ys = xs @ ys;
 
 fun apply [] x = x