diff -r 3f76ae637f71 -r 9d121b171a0a doc-src/IsarImplementation/Thy/logic.thy
--- 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.