--- a/doc-src/IsarImplementation/Thy/logic.thy Wed Sep 03 12:11:28 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy Wed Sep 03 17:47:30 2008 +0200
@@ -326,7 +326,7 @@
@{index_ML fastype_of: "term -> typ"} \\
@{index_ML lambda: "term -> term -> term"} \\
@{index_ML betapply: "term * term -> term"} \\
- @{index_ML Sign.declare_const: "Properties.T -> bstring * typ * mixfix ->
+ @{index_ML Sign.declare_const: "Properties.T -> (Name.binding * typ) * mixfix ->
theory -> term * theory"} \\
@{index_ML Sign.add_abbrev: "string -> Properties.T -> bstring * term ->
theory -> (term * term) * theory"} \\
@@ -374,7 +374,7 @@
"t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
abstraction.
- \item @{ML Sign.declare_const}~@{text "properties (c, \<sigma>, mx)"}
+ \item @{ML Sign.declare_const}~@{text "properties ((c, \<sigma>), mx)"}
declares a new constant @{text "c :: \<sigma>"} with optional mixfix
syntax.