1.1 --- a/doc-src/Codegen/Thy/document/ML.tex	Thu May 14 15:09:47 2009 +0200
     1.2 +++ b/doc-src/Codegen/Thy/document/ML.tex	Thu May 14 15:09:48 2009 +0200
     1.3 @@ -124,16 +124,16 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  \begin{mldecls}
     1.7 -  \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
     1.8 -  \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\
     1.9 +  \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code.read_const: theory -> string -> string| \\
    1.10 +  \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\
    1.11    \end{mldecls}
    1.12  
    1.13    \begin{description}
    1.14  
    1.15 -  \item \verb|Code_Unit.read_const|~\isa{thy}~\isa{s}
    1.16 +  \item \verb|Code.read_const|~\isa{thy}~\isa{s}
    1.17       reads a constant as a concrete term expression \isa{s}.
    1.18  
    1.19 -  \item \verb|Code_Unit.rewrite_eqn|~\isa{ss}~\isa{thm}
    1.20 +  \item \verb|Code.rewrite_eqn|~\isa{ss}~\isa{thm}
    1.21       rewrites a code equation \isa{thm} with a simpset \isa{ss};
    1.22       only arguments and right hand side are rewritten,
    1.23       not the head of the code equation.