--- a/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex Thu Jan 01 21:28:38 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex Thu Jan 01 21:30:13 2009 +0100
@@ -54,9 +54,9 @@
\begin{mldecls}
\indexml{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
\indexml{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
- \indexml{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory| \\
- \indexml{Code.map\_pre}\verb|Code.map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
- \indexml{Code.map\_post}\verb|Code.map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
+ \indexml{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list lazy -> theory -> theory| \\
+ \indexml{Code.map\_pre}\verb|Code.map_pre: (simpset -> simpset) -> theory -> theory| \\
+ \indexml{Code.map\_post}\verb|Code.map_post: (simpset -> simpset) -> theory -> theory| \\
\indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
\verb| -> theory -> theory| \\
\indexml{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
@@ -126,7 +126,7 @@
\begin{mldecls}
\indexml{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
\indexml{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\
- \indexml{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: MetaSimplifier.simpset -> thm -> thm| \\
+ \indexml{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\
\end{mldecls}
\begin{description}