# HG changeset patch
# User wenzelm
# Date 1220371283 -7200
# Node ID db584d1d2af4a7ef778a4eae4e52266a5f4b42c0
# Parent  914183e229e95fa6e7b368cb15979d5ed716f71e
updated generated file;

diff -r 914183e229e9 -r db584d1d2af4 doc-src/IsarImplementation/Thy/document/ML.tex
--- 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}
diff -r 914183e229e9 -r db584d1d2af4 doc-src/IsarImplementation/Thy/document/logic.tex
--- 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| \\