diff -r 7b34c51b05a4 -r 9cea8a0e925a doc-src/Codegen/Thy/document/Inductive_Predicate.tex
--- 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