src/HOL/Tools/dseq.ML

--- a/src/HOL/Tools/dseq.ML	Tue Nov 06 13:12:48 2007 +0100
+++ b/src/HOL/Tools/dseq.ML	Tue Nov 06 13:12:49 2007 +0100
@@ -5,9 +5,27 @@
 Sequences with recursion depth limit.
 *)
 
-structure DSeq =
+signature DSEQ =
+sig
+  type 'a seq = int -> 'a Seq.seq;
+  val maps: ('a -> 'b seq) -> 'a seq -> 'b seq
+  val map: ('a -> 'b) -> 'a seq -> 'b seq
+  val append: 'a seq -> 'a seq -> 'a seq
+  val interleave: 'a seq -> 'a seq -> 'a seq
+  val single: 'a -> 'a seq
+  val empty: 'a seq
+  val guard: bool -> unit seq
+  val of_list: 'a list -> 'a seq
+  val list_of: 'a seq -> 'a list
+  val pull: 'a seq -> ('a * 'a seq) option
+  val hd: 'a seq -> 'a
+end;
+
+structure DSeq : DSEQ =
 struct
 
+type 'a seq = int -> 'a Seq.seq;
+
 fun maps f s 0 = Seq.empty
   | maps f s i = Seq.maps (fn a => f a i) (s (i - 1));
 
@@ -27,7 +45,7 @@
 
 fun list_of s = Seq.list_of (s ~1);
 
-fun pull s = Seq.pull (s ~1);
+fun pull s = Seq.pull (s ~1) |> (Option.map o apsnd) K; (*FIXME*)
 
 fun hd s = Seq.hd (s ~1);