1.1 --- a/src/Pure/General/seq.ML	Thu Sep 24 21:32:12 1998 +0200
     1.2 +++ b/src/Pure/General/seq.ML	Fri Sep 25 12:01:47 1998 +0200
     1.3 @@ -37,6 +37,7 @@
     1.4    val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
     1.5    val TRY: ('a -> 'a seq) -> 'a -> 'a seq
     1.6    val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
     1.7 +  val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
     1.8  end;
     1.9  
    1.10  structure Seq: SEQ =
    1.11 @@ -200,5 +201,7 @@
    1.12            | Some (x, q) => rep (q :: qs) x);
    1.13    in fn x => make (fn () => rep [] x) end;
    1.14  
    1.15 +fun REPEAT1 f = THEN (f, REPEAT f);
    1.16 +
    1.17  
    1.18  end;