# HG changeset patch
# User haftmann
# Date 1242285393 -7200
# Node ID 03a87478b89e40484dd238c11ef0761462710418
# Parent  bdc1504ad456d4e7e81867625c4479229a1d4ff9
updated generated document

diff -r bdc1504ad456 -r 03a87478b89e doc-src/Codegen/Thy/document/Adaptation.tex
--- a/doc-src/Codegen/Thy/document/Adaptation.tex	Thu May 14 08:22:07 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex	Thu May 14 09:16:33 2009 +0200
@@ -166,7 +166,7 @@
        \isa{index} which is mapped to target-language built-in integers.
        Useful for code setups which involve e.g. indexing of
        target-language arrays.
-    \item[\hyperlink{theory.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype
+    \item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype
        \isa{message{\isacharunderscore}string} which is isomorphic to strings;
        \isa{message{\isacharunderscore}string}s are mapped to target-language strings.
        Useful for code setups which involve e.g. printing (error) messages.
diff -r bdc1504ad456 -r 03a87478b89e doc-src/Codegen/Thy/document/ML.tex
--- a/doc-src/Codegen/Thy/document/ML.tex	Thu May 14 08:22:07 2009 +0200
+++ b/doc-src/Codegen/Thy/document/ML.tex	Thu May 14 09:16:33 2009 +0200
@@ -55,11 +55,11 @@
   \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
   \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
   \indexdef{}{ML}{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list lazy -> theory -> theory| \\
-  \indexdef{}{ML}{Code.map\_pre}\verb|Code.map_pre: (simpset -> simpset) -> theory -> theory| \\
-  \indexdef{}{ML}{Code.map\_post}\verb|Code.map_post: (simpset -> simpset) -> theory -> theory| \\
-  \indexdef{}{ML}{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
+  \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
+  \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
+  \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
 \verb|    -> theory -> theory| \\
-  \indexdef{}{ML}{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
+  \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
   \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
   \indexdef{}{ML}{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
 \verb|    -> (string * sort) list * (string * typ list) list| \\
@@ -78,10 +78,10 @@
      suspended code equations \isa{lthms} for constant
      \isa{const} to executable content.
 
-  \item \verb|Code.map_pre|~\isa{f}~\isa{thy} changes
+  \item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes
      the preprocessor simpset.
 
-  \item \verb|Code.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
+  \item \verb|Code_Preproc.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
      function transformer \isa{f} (named \isa{name}) to executable content;
      \isa{f} is a transformer of the code equations belonging
      to a certain function definition, depending on the
@@ -89,7 +89,7 @@
      transformation took place;  otherwise, the whole process will be iterated
      with the new code equations.
 
-  \item \verb|Code.del_functrans|~\isa{name}~\isa{thy} removes
+  \item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes
      function transformer named \isa{name} from executable content.
 
   \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
@@ -125,7 +125,6 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
-  \indexdef{}{ML}{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\
   \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\
   \end{mldecls}
 
@@ -134,9 +133,6 @@
   \item \verb|Code_Unit.read_const|~\isa{thy}~\isa{s}
      reads a constant as a concrete term expression \isa{s}.
 
-  \item \verb|Code_Unit.head_eqn|~\isa{thy}~\isa{thm}
-     extracts the constant and its type from a code equation \isa{thm}.
-
   \item \verb|Code_Unit.rewrite_eqn|~\isa{ss}~\isa{thm}
      rewrites a code equation \isa{thm} with a simpset \isa{ss};
      only arguments and right hand side are rewritten,
diff -r bdc1504ad456 -r 03a87478b89e doc-src/Codegen/Thy/document/Program.tex
--- a/doc-src/Codegen/Thy/document/Program.tex	Thu May 14 08:22:07 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Program.tex	Thu May 14 09:16:33 2009 +0200
@@ -891,8 +891,8 @@
 \hspace*{0pt}fun null [] = true\\
 \hspace*{0pt} ~| null (x ::~xs) = false;\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun eq{\char95}nat (Suc a) Zero{\char95}nat = false\\
-\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc a) = false\\
+\hspace*{0pt}fun eq{\char95}nat (Suc nat') Zero{\char95}nat = false\\
+\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc nat') = false\\
 \hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\
 \hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\
 \hspace*{0pt}\\