--- 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