# HG changeset patch
# User wenzelm
# Date 1142370453 -3600
# Node ID 05b6d220e5091df477e3ce0e2ac1c6b39a3b2f13
# Parent  5f376320109a8d5387ea7e774ed0e0806a0f9113
added singleton;

diff -r 5f376320109a -r 05b6d220e509 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Mar 14 22:06:43 2006 +0100
+++ b/src/Pure/library.ML	Tue Mar 14 22:07:33 2006 +0100
@@ -104,6 +104,7 @@
   exception UnequalLengths
   val cons: 'a -> 'a list -> 'a list
   val single: 'a -> 'a list
+  val singleton: ('a list -> 'b list) -> 'a -> 'b
   val append: 'a list -> 'a list -> 'a list
   val apply: ('a -> 'a) list -> 'a -> 'a
   val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
@@ -493,6 +494,8 @@
 fun cons x xs = x :: xs;
 fun single x = [x];
 
+fun singleton f x = (case f [x] of [y] => y | _ => raise Empty);
+
 fun append xs ys = xs @ ys;
 
 fun apply [] x = x