diff -r 7ffc131909e5 -r 83759063fbbd src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Thu Jul 08 18:29:07 1999 +0200
+++ b/src/Pure/General/seq.ML	Thu Jul 08 18:29:30 1999 +0200
@@ -28,6 +28,7 @@
   val interleave: 'a seq * 'a seq -> 'a 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 succeed: 'a -> 'a seq
   val fail: 'a -> 'b seq
   val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
@@ -163,6 +164,18 @@
         | 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))))));
+
 
 
 (** sequence functions **)      (*some code duplicated from Pure/tctical.ML*)