doc-src/Logics/HOL.tex

   f~x_1~\dots~x_m~(C~y_1~\dots~y_k)~z_1~\dots~z_n = r \] such that $C$ is a
   constructor of the datatype, $r$ contains only the free variables on the
   left-hand side, and all recursive calls in $r$ are of the form
   $f~\dots~y_i~\dots$ for some $i$. There must be exactly one reduction
   rule for each constructor. Since these reduction rules are mainly used via
-  the implicit simpset, their identifiers may also be omitted.
+  the implicit simpset, their names may be omitted.
 \end{itemize}
 A theory file may contain any number of {\tt primrec} sections which may be
 intermixed with other declarations.
 
 For the consistency-sensitive user it may be reassuring to know that {\tt