# HG changeset patch
# User wenzelm
# Date 1154619040 -7200
# Node ID 27e4f43a0c3ebf8aa29bbb21296ee262143eaaef
# Parent  ccdd1592f5ffa0a52655e731ca76cc2d1c7e51d9
removed obsolete commute, map_list;

diff -r ccdd1592f5ff -r 27e4f43a0c3e src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Thu Aug 03 17:30:39 2006 +0200
+++ b/src/Pure/General/seq.ML	Thu Aug 03 17:30:40 2006 +0200
@@ -35,8 +35,6 @@
   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
-  val map_list: ('a -> 'b seq) -> 'a list -> 'b list seq
   val succeed: 'a -> 'a seq
   val fail: 'a -> 'b seq
   val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
@@ -187,20 +185,6 @@
         | SOME (a, s') => pull (f (a, its s'))))
   in its xq end;
 
-(*turn a list of sequences into a sequence of lists*)
-fun commute [] = single []
-  | commute (xq :: xqs) =
-      make (fn () =>
-        (case pull xq of
-          NONE => NONE
-        | SOME (x, xq') =>
-            (case pull (commute xqs) of
-              NONE => NONE
-            | SOME (xs, xsq) =>
-                SOME (x :: xs, append (map (Library.cons x) xsq) (commute (xq' :: xqs))))));
-
-fun map_list f = commute o List.map f;
-
 
 
 (** sequence functions **)      (*some code copied from Pure/tctical.ML*)