--- a/src/Pure/library.ML Mon Jul 17 01:28:17 2006 +0200
+++ b/src/Pure/library.ML Mon Jul 17 15:16:17 2006 +0200
@@ -103,7 +103,6 @@
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
@@ -497,10 +496,6 @@
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