# HG changeset patch
# User wenzelm
# Date 1150565873 -7200
# Node ID 4a3e35fd6e028b246ce142b4b85576a0a3060fd2
# Parent  300bc6ce970d53095819cdddd0ae388575868551
added singleton;

diff -r 300bc6ce970d -r 4a3e35fd6e02 src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Sat Jun 17 19:37:52 2006 +0200
+++ b/src/Pure/General/seq.ML	Sat Jun 17 19:37:53 2006 +0200
@@ -32,6 +32,7 @@
   val map_filter: ('a -> 'b option) -> 'a seq -> 'b seq
   val lift: ('a -> 'b -> 'c) -> 'a seq -> 'b -> 'c seq
   val lifts: ('a -> 'b -> 'c seq) -> 'a seq -> 'b -> 'c seq
+  val singleton: ('a list -> 'b list seq) -> 'a -> 'b seq
   val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
   val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
   val commute: 'a seq list -> 'a list seq
@@ -162,6 +163,9 @@
 fun lift f xq y = map (fn x => f x y) xq;
 fun lifts f xq y = maps (fn x => f x y) xq;
 
+fun singleton f x = f [x] |> map (fn [y] => y | _ => raise Empty);
+
+
 (*print a sequence, up to "count" elements*)
 fun print print_elem count =
   let