1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Jul 15 15:59:49 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Jul 15 16:02:07 2008 +0200
     1.3 @@ -501,8 +501,8 @@
     1.4  text {*
     1.5    Before selected function theorems are turned into abstract
     1.6    code, a chain of definitional transformation steps is carried
     1.7 -  out: \emph{preprocessing}.  In essence, the preprocessort
     1.8 -  consists of two components: a \emph{simpset} and \emph{function transformators}.
     1.9 +  out: \emph{preprocessing}.  In essence, the preprocessor
    1.10 +  consists of two components: a \emph{simpset} and \emph{function transformers}.
    1.11  
    1.12    The \emph{simpset} allows to employ the full generality of the Isabelle
    1.13    simplifier.  Due to the interpretation of theorems
    1.14 @@ -546,22 +546,19 @@
    1.15  
    1.16  text {*
    1.17  
    1.18 -  \emph{Function transformators} provide a most general interface,
    1.19 +  \emph{Function transformers} provide a very general interface,
    1.20    transforming a list of function theorems to another
    1.21    list of function theorems, provided that neither the heading
    1.22    constant nor its type change.  The @{term "0\<Colon>nat"} / @{const Suc}
    1.23    pattern elimination implemented in
    1.24 -  theory @{text "EfficientNat"} (\secref{eff_nat}) uses this
    1.25 +  theory @{text "Efficient_Nat"} (\secref{eff_nat}) uses this
    1.26    interface.
    1.27  
    1.28    \noindent The current setup of the preprocessor may be inspected using
    1.29    the @{text "\<PRINTCODESETUP>"} command.
    1.30  
    1.31    \begin{warn}
    1.32 -    Preprocessing is \emph{no} fix point process.  Keep this in mind when
    1.33 -    setting up the preprocessor.
    1.34 -
    1.35 -    Further, the attribute \emph{code unfold}
    1.36 +    The attribute \emph{code unfold}
    1.37      associated with the existing code generator also applies to
    1.38      the new one: \emph{code unfold} implies \emph{code inline}.
    1.39    \end{warn}
    1.40 @@ -1096,7 +1093,7 @@
    1.41    @{index_ML Code.add_funcl: "string * thm list Susp.T -> theory -> theory"} \\
    1.42    @{index_ML Code.map_pre: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
    1.43    @{index_ML Code.map_post: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
    1.44 -  @{index_ML Code.add_functrans: "string * (theory -> thm list -> thm list)
    1.45 +  @{index_ML Code.add_functrans: "string * (theory -> thm list -> thm list option)
    1.46      -> theory -> theory"} \\
    1.47    @{index_ML Code.del_functrans: "string -> theory -> theory"} \\
    1.48    @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
    1.49 @@ -1120,14 +1117,16 @@
    1.50    \item @{ML Code.map_pre}~@{text "f"}~@{text "thy"} changes
    1.51       the preprocessor simpset.
    1.52  
    1.53 -    \item @{ML Code.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
    1.54 -     function transformator @{text f} (named @{text name}) to executable content;
    1.55 -     @{text f} is a transformation of the defining equations belonging
    1.56 +  \item @{ML Code.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
    1.57 +     function transformer @{text f} (named @{text name}) to executable content;
    1.58 +     @{text f} is a transformer of the defining equations belonging
    1.59       to a certain function definition, depending on the
    1.60 -     current theory context.
    1.61 +     current theory context.  Returning @{text NONE} indicates that no
    1.62 +     transformation took place;  otherwise, the whole process will be iterated
    1.63 +     with the new defining equations.
    1.64  
    1.65    \item @{ML Code.del_functrans}~@{text "name"}~@{text "thy"} removes
    1.66 -     function transformator named @{text name} from executable content.
    1.67 +     function transformer named @{text name} from executable content.
    1.68  
    1.69    \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
    1.70       a datatype to executable content, with generation