diff -r 06728ef076a7 -r 7b34c51b05a4 doc-src/Codegen/Thy/Inductive_Predicate.thy
--- a/doc-src/Codegen/Thy/Inductive_Predicate.thy	Wed Aug 18 10:07:56 2010 +0200
+++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy	Wed Aug 18 10:07:56 2010 +0200
@@ -16,7 +16,7 @@
 section {* Inductive Predicates \label{sec:inductive} *}
 
 text {*
-  The @{text predicate_compiler} is an extension of the code generator
+  The @{text "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