--- a/doc-src/IsarImplementation/Thy/document/ML.tex Tue Sep 02 17:31:20 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue Sep 02 18:01:23 2008 +0200
@@ -369,7 +369,7 @@
a theory by constant declararion and primitive definitions:
\smallskip\begin{mldecls}
- \verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix|\isasep\isanewline%
+ \verb|Sign.declare_const: Properties.T -> bstring * typ * mixfix|\isasep\isanewline%
\verb| -> theory -> term * theory| \\
\verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory|
\end{mldecls}
--- a/doc-src/IsarImplementation/Thy/document/logic.tex Tue Sep 02 17:31:20 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Tue Sep 02 18:01:23 2008 +0200
@@ -328,9 +328,9 @@
\indexml{fastype\_of}\verb|fastype_of: term -> typ| \\
\indexml{lambda}\verb|lambda: term -> term -> term| \\
\indexml{betapply}\verb|betapply: term * term -> term| \\
- \indexml{Sign.declare\_const}\verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix ->|\isasep\isanewline%
+ \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> bstring * typ * mixfix ->|\isasep\isanewline%
\verb| theory -> term * theory| \\
- \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Markup.property list -> bstring * term ->|\isasep\isanewline%
+ \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> bstring * term ->|\isasep\isanewline%
\verb| theory -> (term * term) * theory| \\
\indexml{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
\indexml{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\