--- a/doc-src/Codegen/Thy/ML.thy Tue Jul 14 10:54:04 2009 +0200
+++ b/doc-src/Codegen/Thy/ML.thy Tue Jul 14 10:54:21 2009 +0200
@@ -78,8 +78,7 @@
text %mlref {*
\begin{mldecls}
- @{index_ML Code.read_const: "theory -> string -> string"} \\
- @{index_ML Code.rewrite_eqn: "simpset -> thm -> thm"} \\
+ @{index_ML Code.read_const: "theory -> string -> string"}
\end{mldecls}
\begin{description}
@@ -87,11 +86,6 @@
\item @{ML Code.read_const}~@{text thy}~@{text s}
reads a constant as a concrete term expression @{text s}.
- \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.
-
\end{description}
*}