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