doc-src/Codegen/Thy/document/Foundations.tex

 \begin{isamarkuptext}%
 \noindent \emph{Function transformers} provide a very general
   interface, transforming a list of function theorems to another list
   of function theorems, provided that neither the heading constant nor
   its type change.  The \isa{{\isadigit{0}}} / \isa{Suc} pattern
-  elimination implemented in theory \hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isaliteral{5F}{\isacharunderscore}}Nat}}} (see
+  elimination implemented in theory \isa{Efficient{\isaliteral{5F}{\isacharunderscore}}Nat} (see
   \secref{eff_nat}) uses this interface.
 
   \noindent The current setup of the preprocessor may be inspected
   using the \indexdef{}{command}{print\_codeproc}\hypertarget{command.print-codeproc}{\hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codeproc}}}}} command.  \indexdef{}{command}{code\_thms}\hypertarget{command.code-thms}{\hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}} (see \secref{sec:equations}) provides a convenient
   mechanism to inspect the impact of a preprocessor setup on code