diff -r d6ceb4275742 -r 64a8495201d1 src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Thu Sep 24 21:32:12 1998 +0200
+++ b/src/Pure/General/seq.ML	Fri Sep 25 12:01:47 1998 +0200
@@ -37,6 +37,7 @@
   val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
   val TRY: ('a -> 'a seq) -> 'a -> 'a seq
   val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
+  val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
 end;
 
 structure Seq: SEQ =
@@ -200,5 +201,7 @@
           | Some (x, q) => rep (q :: qs) x);
   in fn x => make (fn () => rep [] x) end;
 
+fun REPEAT1 f = THEN (f, REPEAT f);
+
 
 end;