Protected underscore in inductive_set.

--- a/doc-src/TutorialI/Inductive/Even.thy	Mon Jul 23 14:36:37 2007 +0200
+++ b/doc-src/TutorialI/Inductive/Even.thy	Mon Jul 23 14:39:21 2007 +0200
@@ -16,7 +16,7 @@
 subsection{* Making an Inductive Definition *}
 
 text {*
-Using \commdx{inductive\_set}, we declare the constant @{text even} to be
+Using \commdx{inductive\protect\_set}, we declare the constant @{text even} to be
 a set of natural numbers with the desired properties.
 *}
 

--- a/doc-src/TutorialI/Inductive/document/Even.tex	Mon Jul 23 14:36:37 2007 +0200
+++ b/doc-src/TutorialI/Inductive/document/Even.tex	Mon Jul 23 14:39:21 2007 +0200
@@ -35,7 +35,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Using \commdx{inductive\_set}, we declare the constant \isa{even} to be
+Using \commdx{inductive\protect\_set}, we declare the constant \isa{even} to be
 a set of natural numbers with the desired properties.%
 \end{isamarkuptext}%
 \isamarkuptrue%