--- a/doc-src/IsarImplementation/Thy/document/ML.tex Wed Jan 21 16:47:31 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Wed Jan 21 16:47:32 2009 +0100
@@ -366,7 +366,7 @@
a theory by constant declararion and primitive definitions:
\smallskip\begin{mldecls}
- \verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix|\isasep\isanewline%
+ \verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix|\isasep\isanewline%
\verb| -> theory -> term * theory| \\
\verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory|
\end{mldecls}