
diff -r 92d8ff6af82c -r 90fed3d4430f doc-src/Codegen/Thy/ML.thy
--- a/doc-src/Codegen/Thy/ML.thy	Thu May 14 15:09:47 2009 +0200
+++ b/doc-src/Codegen/Thy/ML.thy	Thu May 14 15:09:48 2009 +0200
@@ -78,16 +78,16 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML Code_Unit.read_const: "theory -> string -> string"} \\
-  @{index_ML Code_Unit.rewrite_eqn: "simpset -> thm -> thm"} \\
+  @{index_ML Code.read_const: "theory -> string -> string"} \\
+  @{index_ML Code.rewrite_eqn: "simpset -> thm -> thm"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML Code_Unit.read_const}~@{text thy}~@{text s}
+  \item @{ML Code.read_const}~@{text thy}~@{text s}
      reads a constant as a concrete term expression @{text s}.
 
-  \item @{ML Code_Unit.rewrite_eqn}~@{text ss}~@{text thm}
+  \item @{ML Code.rewrite_eqn}~@{text ss}~@{text thm}
      rewrites a code equation @{text thm} with a simpset @{text ss};
      only arguments and right hand side are rewritten,
      not the head of the code equation.




