doc-src/TutorialI/Sets/sets.tex

 \[ \cdots \prec a@2 \prec a@1 \prec a@0. \]
 Well-foundedness can be hard to show. The various 
 formulations are all complicated.  However,  often a relation
 is well-founded by construction.  HOL provides
 theorems concerning ways of constructing  a well-founded relation.  The
-most familiar way is to specify a \bfindex{measure function}~\isa{f} into
+most familiar way is to specify a 
+\index{measure functions}\textbf{measure function}~\isa{f} into
 the natural numbers, when $\isa{x}\prec \isa{y}\iff \isa{f x} < \isa{f y}$;
 we write this particular relation as
 \isa{measure~f}.
 
 \begin{warn}