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}