1.1 --- a/src/Pure/library.ML	Tue Oct 16 19:45:57 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Oct 16 23:12:38 2007 +0200
     1.3 @@ -71,6 +71,7 @@
     1.4    val single: 'a -> 'a list
     1.5    val the_single: 'a list -> 'a
     1.6    val singleton: ('a list -> 'b list) -> 'a -> 'b
     1.7 +  val yield_singleton: ('a list -> 'c -> 'b list * 'c) -> 'a -> 'c -> 'b * 'c
     1.8    val apply: ('a -> 'a) list -> 'a -> 'a
     1.9    val perhaps_apply: ('a -> 'a option) list -> 'a -> 'a option
    1.10    val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option
    1.11 @@ -356,6 +357,8 @@
    1.12  
    1.13  fun singleton f x = the_single (f [x]);
    1.14  
    1.15 +fun yield_singleton f x = f [x] #>> the_single;
    1.16 +
    1.17  fun apply [] x = x
    1.18    | apply (f :: fs) x = apply fs (f x);
    1.19