--- a/doc-src/Codegen/Thy/document/Adaptation.tex Wed Aug 18 10:07:56 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Wed Aug 18 10:07:57 2010 +0200
@@ -577,7 +577,7 @@
\begin{isamarkuptext}%
\noindent The code generator would produce an additional instance,
which of course is rejected by the \isa{Haskell} compiler. To
- suppress this additional instance, use \isa{code{\isacharunderscore}instance}:%
+ suppress this additional instance, use \indexdef{}{command}{code\_instance}\hypertarget{command.code-instance}{\hyperlink{command.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Further.tex Wed Aug 18 10:07:56 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Wed Aug 18 10:07:57 2010 +0200
@@ -415,8 +415,9 @@
\indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
- \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
-\verb| -> theory -> theory| \\
+ \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: |\isasep\isanewline%
+\verb| string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
+\verb| -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
\indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
\indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
--- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Wed Aug 18 10:07:56 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Wed Aug 18 10:07:57 2010 +0200
@@ -37,7 +37,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \isa{predicate{\isacharunderscore}compiler} is an extension of the code generator
+The \isa{predicate\ compiler} is an extension of the code generator
which turns inductive specifications into equational ones, from
which in turn executable code can be generated. The mechanisms of
this compiler are described in detail in