1.1 --- a/doc-src/Ref/tctical.tex	Mon May 05 21:18:01 1997 +0200
     1.2 +++ b/doc-src/Ref/tctical.tex	Tue May 06 12:50:16 1997 +0200
     1.3 @@ -126,9 +126,8 @@
     1.4  \begin{ttbox} 
     1.5  fun TRY tac = tac ORELSE all_tac;
     1.6  
     1.7 -fun REPEAT tac = Tactic
     1.8 -     (fn state => tapply((tac THEN REPEAT tac) ORELSE all_tac,
     1.9 -                         state));
    1.10 +fun REPEAT tac =
    1.11 +     (fn state => ((tac THEN REPEAT tac) ORELSE all_tac) state);
    1.12  \end{ttbox}
    1.13  If $tac$ can return multiple outcomes then so can \hbox{\tt REPEAT $tac$}.
    1.14  Since {\tt REPEAT} uses \ttindex{ORELSE} and not {\tt APPEND} or {\tt