# HG changeset patch
# User haftmann
# Date 1282118876 -7200
# Node ID 7b34c51b05a4de634fee2a7b31c39b2e012bad49
# Parent  06728ef076a75227b7699339f3a6f786e8120c32
dropped errorneous underscore

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