--- a/CookBook/Package/Ind_Interface.thy	Tue Mar 17 12:26:34 2009 +0100
+++ b/CookBook/Package/Ind_Interface.thy	Tue Mar 17 17:32:12 2009 +0100
@@ -179,17 +179,17 @@
   are not yet in any way reflected in the introduction rules. So the task of
   @{ML add_inductive in SimpleInductivePackage} is to transform the strings
   into properly typed terms. For this it can use the function 
-  @{ML read_specification in Specification}. This function takes some constants
+  @{ML read_spec in Specification}. This function takes some constants
   with possible typing annotations and some rule specifications and attempts to
   find a type according to the given type constraints and the type constraints
   by the surrounding (local theory). However this function is a bit
   too general for our purposes: we want that each introduction rule has only 
   name (for example @{text even0} or @{text evenS}), if a name is given at all.
-  The function @{ML read_specification in Specification} however allows more
+  The function @{ML read_spec in Specification} however allows more
   than one rule. Since it is quite convenient to rely on this function (instead of
   building your own) we just quick ly write a wrapper function that translates
   between our specific format and the general format expected by 
-  @{ML read_specification in Specification}. The code of this wrapper is as follows:
+  @{ML read_spec in Specification}. The code of this wrapper is as follows:
 
   @{ML_chunk [display,gray,linenos] read_specification}
 
@@ -287,22 +287,22 @@
 text {*
   During parsing, both predicates and parameters are treated as variables, so
   the lists \verb!preds_syn! and \verb!params_syn! are just appended
-  before being passed to @{ML read_specification in Specification}. Note that the format
-  for rules supported by @{ML read_specification in Specification} is more general than
+  before being passed to @{ML read_spec in Specification}. Note that the format
+  for rules supported by @{ML read_spec in Specification} is more general than
   what is required for our package. It allows several rules to be associated
   with one name, and the list of rules can be partitioned into several
   sublists. In order for the list \verb!intro_srcs! of introduction rules
-  to be acceptable as an input for @{ML read_specification in Specification}, we first
+  to be acceptable as an input for @{ML read_spec in Specification}, we first
   have to turn it into a list of singleton lists. This transformation
   has to be reversed later on by applying the function
   @{ML [display] "the_single: 'a list -> 'a"}
   to the list \verb!specs! containing the parsed introduction rules.
-  The function @{ML read_specification in Specification} also returns the list \verb!vars!
+  The function @{ML read_spec in Specification} also returns the list \verb!vars!
   of predicates and parameters that contains the inferred types as well.
   This list has to be chopped into the two lists \verb!preds_syn'! and
   \verb!params_syn'! for predicates and parameters, respectively.
   All variables occurring in a rule but not in the list of variables passed to
-  @{ML read_specification in Specification} will be bound by a meta-level universal
+  @{ML read_spec in Specification} will be bound by a meta-level universal
   quantifier.
 *}