src/Pure/General/seq.ML

--- a/src/Pure/General/seq.ML	Mon Mar 20 18:45:28 2000 +0100
+++ b/src/Pure/General/seq.ML	Mon Mar 20 18:46:53 2000 +0100
@@ -39,6 +39,7 @@
   val TRY: ('a -> 'a seq) -> 'a -> 'a seq
   val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
   val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
+  val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
 end;
 
 structure Seq: SEQ =
@@ -217,4 +218,9 @@
 fun REPEAT1 f = THEN (f, REPEAT f);
 
 
+fun INTERVAL f i j x =
+  if i > j then single x
+  else op THEN (f j, INTERVAL f i (j - 1)) x;
+
+
 end;