diff -r 5a3fa0c4b215 -r 6ddcc24038e1 doc-src/Tutorial/fp.tex
--- a/doc-src/Tutorial/fp.tex	Wed Oct 13 15:18:15 1999 +0200
+++ b/doc-src/Tutorial/fp.tex	Wed Oct 13 15:41:24 1999 +0200
@@ -1356,7 +1356,7 @@
 theorems simultaneously:
 \begin{quote}\small
 \verbatiminput{Datatype/abgoalind.ML}
-\end{quote}\indexbold{*mutual_induct_tac}
+\end{quote}
 The resulting 8 goals (one for each constructor) are proved in one fell swoop
 \texttt{by Auto_tac;}.
 
@@ -1365,7 +1365,7 @@
 \[ P@1(x@1)\ \texttt{\&}\ \dots\ \texttt{\&}\ P@n(x@n) \]
 where each variable $x@i$ is of type $\tau@i$. Induction is started by
 \begin{ttbox}
-by(mutual_induct_tac ["\(x@1\)",\(\dots\),"\(x@n\)"] \(k\));
+by(induct_tac "\(x@1\) \(\dots\) \(x@n\)" \(k\));
 \end{ttbox}
 
 \begin{exercise}