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