--- a/doc-src/TutorialI/ToyList/ToyList.thy Wed Dec 13 09:32:55 2000 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Wed Dec 13 09:39:53 2000 +0100
@@ -69,7 +69,8 @@
\isacommand{primrec}\index{*primrec} indicates that the recursion is of a
particularly primitive kind where each recursive call peels off a datatype
constructor from one of the arguments. Thus the
-recursion always terminates, i.e.\ the function is \bfindex{total}.
+recursion always terminates, i.e.\ the function is \textbf{total}.
+\index{total function}
The termination requirement is absolutely essential in HOL, a logic of total
functions. If we were to drop it, inconsistencies would quickly arise: the