# HG changeset patch
# User haftmann
# Date 1242808656 -7200
# Node ID a9fa62683582ec710c3a1ed76763b1576842485f
# Parent  98370b26c2ce5b11406f65b388c8fe6aaf05878b
adjusted to changed theory name

diff -r 98370b26c2ce -r a9fa62683582 doc-src/Codegen/Thy/Adaptation.thy
--- a/doc-src/Codegen/Thy/Adaptation.thy	Tue May 19 16:54:55 2009 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy	Wed May 20 10:37:36 2009 +0200
@@ -121,8 +121,8 @@
        which in general will result in higher efficiency; pattern
        matching with @{term "0\<Colon>nat"} / @{const "Suc"}
        is eliminated;  includes @{theory "Code_Integer"}
-       and @{theory "Code_Index"}.
-    \item[@{theory "Code_Index"}] provides an additional datatype
+       and @{theory "Code_Numeral"}.
+    \item[@{theory "Code_Numeral"}] provides an additional datatype
        @{typ index} which is mapped to target-language built-in integers.
        Useful for code setups which involve e.g. indexing of
        target-language arrays.
diff -r 98370b26c2ce -r a9fa62683582 doc-src/Codegen/Thy/document/Adaptation.tex
--- a/doc-src/Codegen/Thy/document/Adaptation.tex	Tue May 19 16:54:55 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex	Wed May 20 10:37:36 2009 +0200
@@ -161,14 +161,14 @@
        which in general will result in higher efficiency; pattern
        matching with \isa{{\isadigit{0}}} / \isa{Suc}
        is eliminated;  includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}
-       and \hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}.
-    \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] provides an additional datatype
+       and \hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isacharunderscore}Numeral}}}.
+    \item[\hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isacharunderscore}Numeral}}}] provides an additional datatype
        \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.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.
+       \isa{String{\isachardot}literal} which is isomorphic to strings;
+       \isa{String{\isachardot}literal}s are mapped to target-language strings.
        Useful for code setups which involve e.g. printing (error) messages.
 
   \end{description}
diff -r 98370b26c2ce -r a9fa62683582 doc-src/Codegen/Thy/document/ML.tex
--- a/doc-src/Codegen/Thy/document/ML.tex	Tue May 19 16:54:55 2009 +0200
+++ b/doc-src/Codegen/Thy/document/ML.tex	Wed May 20 10:37:36 2009 +0200
@@ -124,8 +124,8 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code.read_const: theory -> string -> string| \\
-  \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\
+  \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| \\
+  \indexdef{}{ML}{Code.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\
   \end{mldecls}
 
   \begin{description}