added singleton;
authorwenzelm
Tue Mar 14 22:07:33 2006 +0100 (2006-03-14)
changeset 1927305b6d220e509
parent 19272 5f376320109a
child 19274 b85e16bd70d0
added singleton;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Mar 14 22:06:43 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Mar 14 22:07:33 2006 +0100
     1.3 @@ -104,6 +104,7 @@
     1.4    exception UnequalLengths
     1.5    val cons: 'a -> 'a list -> 'a list
     1.6    val single: 'a -> 'a list
     1.7 +  val singleton: ('a list -> 'b list) -> 'a -> 'b
     1.8    val append: 'a list -> 'a list -> 'a list
     1.9    val apply: ('a -> 'a) list -> 'a -> 'a
    1.10    val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.11 @@ -493,6 +494,8 @@
    1.12  fun cons x xs = x :: xs;
    1.13  fun single x = [x];
    1.14  
    1.15 +fun singleton f x = (case f [x] of [y] => y | _ => raise Empty);
    1.16 +
    1.17  fun append xs ys = xs @ ys;
    1.18  
    1.19  fun apply [] x = x