# HG changeset patch
# User haftmann
# Date 1224837675 -7200
# Node ID f1c76cf109158b9a95eb970b2d78c87a63b717ee
# Parent  d7384e8e99b3540f0e27aac2875be206d823d7a4
updated

diff -r d7384e8e99b3 -r f1c76cf10915 doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex	Fri Oct 24 10:41:13 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex	Fri Oct 24 10:41:15 2008 +0200
@@ -54,7 +54,7 @@
 \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 Susp.T -> 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\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%