src/Pure/General/seq.ML
changeset 20332 27e4f43a0c3e
parent 19912 4a3e35fd6e02
child 21270 b82f4c16355e
     1.1 --- a/src/Pure/General/seq.ML	Thu Aug 03 17:30:39 2006 +0200
     1.2 +++ b/src/Pure/General/seq.ML	Thu Aug 03 17:30:40 2006 +0200
     1.3 @@ -35,8 +35,6 @@
     1.4    val singleton: ('a list -> 'b list seq) -> 'a -> 'b seq
     1.5    val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
     1.6    val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
     1.7 -  val commute: 'a seq list -> 'a list seq
     1.8 -  val map_list: ('a -> 'b seq) -> 'a list -> 'b list seq
     1.9    val succeed: 'a -> 'a seq
    1.10    val fail: 'a -> 'b seq
    1.11    val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
    1.12 @@ -187,20 +185,6 @@
    1.13          | SOME (a, s') => pull (f (a, its s'))))
    1.14    in its xq end;
    1.15  
    1.16 -(*turn a list of sequences into a sequence of lists*)
    1.17 -fun commute [] = single []
    1.18 -  | commute (xq :: xqs) =
    1.19 -      make (fn () =>
    1.20 -        (case pull xq of
    1.21 -          NONE => NONE
    1.22 -        | SOME (x, xq') =>
    1.23 -            (case pull (commute xqs) of
    1.24 -              NONE => NONE
    1.25 -            | SOME (xs, xsq) =>
    1.26 -                SOME (x :: xs, append (map (Library.cons x) xsq) (commute (xq' :: xqs))))));
    1.27 -
    1.28 -fun map_list f = commute o List.map f;
    1.29 -
    1.30  
    1.31  
    1.32  (** sequence functions **)      (*some code copied from Pure/tctical.ML*)