--- 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}