--- 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