diff -r 796c6ea633b3 -r 5f003fdf2653 CookBook/Package/Ind_Interface.thy
--- a/CookBook/Package/Ind_Interface.thy	Sat Feb 14 00:24:05 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Sat Feb 14 13:20:21 2009 +0000
@@ -108,11 +108,23 @@
 text {*
   The syntax of the \simpleinductive{} command can be described by the
   railroad diagram in Figure~\ref{fig:railroad}. This diagram more or less
-  translates directly into the parser
+  translates directly into the parser:
+
+  @{ML_chunk [display,gray] parser}
+
+  which we also described in Section~\ref{sec:parsingspecs}. Its return value
+  of this parser is a locale, the predicates, parameters and specifications of 
+  the introduction rules. This is all the information we need to call the package. 
 
-   @{ML_chunk [display,gray,linenos] parser}
+  @{ML_chunk [display,gray,linenos] syntax}
 
-  which we also described in Section~\ref{sec:parsingspecs}
+  The locale is passed as argument to the function 
+  @{ML Toplevel.local_theory}.\footnote{FIXME Is this already described?} The
+  other arguments, i.e.~the predicates, parameters and specifications, are passed
+  to the function @{ML add_inductive in SimpleInductivePackage} (Line 4). The
+  actual command is defined in Lines 6 and 7. We called @{ML OuterSyntax.command}
+  with the kind-indicator @{ML OuterKeyword.thy_decl} since the package does
+  not need to open up any goal state (see Section~\ref{sec:newcommand}).
 
   In order to add a new inductive predicate to a theory with the help of our
   package, the user must \emph{invoke} it. For every package, there are
@@ -305,27 +317,6 @@
   \isa{\isacommand{simple{\isacharunderscore}inductive}} command:
   
  
-
-  The definition of the parser \verb!ind_decl! closely follows the railroad
-  diagram shown above. In order to make the code more readable, the structures
-  @{ML_struct OuterParse} and @{ML_struct OuterKeyword} are abbreviated by
-  \texttt{P} and \texttt{K}, respectively. Note how the parser combinator
-  @{ML "!!!" in OuterParse} is used: once the keyword \texttt{where}
-  has been parsed, a non-empty list of introduction rules must follow.
-  Had we not used the combinator @{ML "!!!" in OuterParse}, a
-  \texttt{where} not followed by a list of rules would have caused the parser
-  to respond with the somewhat misleading error message
-
-  \begin{verbatim}
-  Outer syntax error: end of input expected, but keyword where was found
-  \end{verbatim}
-
-  rather than with the more instructive message
-
-  \begin{verbatim}
-  Outer syntax error: proposition expected, but terminator was found
-  \end{verbatim}
-
   Once all arguments of the command have been parsed, we apply the function
   @{ML add_inductive in SimpleInductivePackage}, which yields a local theory
   transformer of type @{ML_type "local_theory -> local_theory"}. Commands in