# HG changeset patch
# User wenzelm
# Date 1160177470 -7200
# Node ID 90b3f8047f554149a11f5654ce5453c53fea4f3a
# Parent  54481abec257448582287a24a9a682efe6961ead
added the_single;

diff -r 54481abec257 -r 90b3f8047f55 src/Pure/library.ML
--- a/src/Pure/library.ML	Sat Oct 07 01:31:09 2006 +0200
+++ b/src/Pure/library.ML	Sat Oct 07 01:31:10 2006 +0200
@@ -102,6 +102,7 @@
   exception UnequalLengths
   val cons: 'a -> 'a list -> 'a list
   val single: 'a -> 'a list
+  val the_single: 'a list -> 'a
   val singleton: ('a list -> 'b list) -> 'a -> 'b
   val append: 'a list -> 'a list -> 'a list
   val apply: ('a -> 'a) list -> 'a -> 'a
@@ -488,9 +489,13 @@
 exception UnequalLengths;
 
 fun cons x xs = x :: xs;
+
 fun single x = [x];
 
-fun singleton f x = (case f [x] of [y] => y | _ => raise Empty);
+fun the_single [x] = x
+  | the_single _ = raise Empty;
+
+fun singleton f x = the_single (f [x]);
 
 fun append xs ys = xs @ ys;