--- a/doc-src/IsarImplementation/Thy/ML.thy Wed Aug 27 11:24:35 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Wed Aug 27 11:48:54 2008 +0200
@@ -317,7 +317,7 @@
a theory by constant declararion and primitive definitions:
\smallskip\begin{mldecls}
- @{ML "Sign.declare_const: Markup.property list -> bstring * typ * mixfix
+ @{ML "Sign.declare_const: Properties.T -> bstring * typ * mixfix
-> theory -> term * theory"} \\
@{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
\end{mldecls}