doc-src/Ref/simplifier.tex
changeset 15027 d23887300b96
parent 13938 b033b53d0c1e
child 16019 0e1405402d53
--- a/doc-src/Ref/simplifier.tex	Thu Jul 08 19:34:18 2004 +0200
+++ b/doc-src/Ref/simplifier.tex	Thu Jul 08 19:34:56 2004 +0200
@@ -1143,9 +1143,9 @@
 \section{*Coding simplification procedures}
 \begin{ttbox}
   val Simplifier.simproc: Sign.sg -> string -> string list
-    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
+    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
   val Simplifier.simproc_i: Sign.sg -> string -> term list
-    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
+    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
 \end{ttbox}
 
 \begin{ttdescription}