diff -r 55f33da63366 -r 458068404143 doc-src/TutorialI/ToyList/ToyList.thy
--- 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