# HG changeset patch
# User haftmann
# Date 1192569158 -7200
# Node ID 250e1da3204b36bdd55f9a4b764514db18c175e3
# Parent  17c313217998b58f8b2bcf81c37992aa8e134f0f
added yield_singleton

diff -r 17c313217998 -r 250e1da3204b src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Oct 16 19:45:57 2007 +0200
+++ b/src/Pure/library.ML	Tue Oct 16 23:12:38 2007 +0200
@@ -71,6 +71,7 @@
   val single: 'a -> 'a list
   val the_single: 'a list -> 'a
   val singleton: ('a list -> 'b list) -> 'a -> 'b
+  val yield_singleton: ('a list -> 'c -> 'b list * 'c) -> 'a -> 'c -> 'b * 'c
   val apply: ('a -> 'a) list -> 'a -> 'a
   val perhaps_apply: ('a -> 'a option) list -> 'a -> 'a option
   val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option
@@ -356,6 +357,8 @@
 
 fun singleton f x = the_single (f [x]);
 
+fun yield_singleton f x = f [x] #>> the_single;
+
 fun apply [] x = x
   | apply (f :: fs) x = apply fs (f x);