src/Pure/General/seq.ML
changeset 19912 4a3e35fd6e02
parent 19865 8e1cee9e03dc
child 20332 27e4f43a0c3e
     1.1 --- a/src/Pure/General/seq.ML	Sat Jun 17 19:37:52 2006 +0200
     1.2 +++ b/src/Pure/General/seq.ML	Sat Jun 17 19:37:53 2006 +0200
     1.3 @@ -32,6 +32,7 @@
     1.4    val map_filter: ('a -> 'b option) -> 'a seq -> 'b seq
     1.5    val lift: ('a -> 'b -> 'c) -> 'a seq -> 'b -> 'c seq
     1.6    val lifts: ('a -> 'b -> 'c seq) -> 'a seq -> 'b -> 'c seq
     1.7 +  val singleton: ('a list -> 'b list seq) -> 'a -> 'b seq
     1.8    val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
     1.9    val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
    1.10    val commute: 'a seq list -> 'a list seq
    1.11 @@ -162,6 +163,9 @@
    1.12  fun lift f xq y = map (fn x => f x y) xq;
    1.13  fun lifts f xq y = maps (fn x => f x y) xq;
    1.14  
    1.15 +fun singleton f x = f [x] |> map (fn [y] => y | _ => raise Empty);
    1.16 +
    1.17 +
    1.18  (*print a sequence, up to "count" elements*)
    1.19  fun print print_elem count =
    1.20    let