--- a/doc-src/IsarImplementation/Thy/document/logic.tex Thu Nov 20 22:39:12 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Fri Nov 21 07:34:36 2008 +0100
@@ -330,7 +330,7 @@
\indexml{betapply}\verb|betapply: term * term -> term| \\
\indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (Name.binding * typ) * mixfix ->|\isasep\isanewline%
\verb| theory -> term * theory| \\
- \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> bstring * term ->|\isasep\isanewline%
+ \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> Name.binding * 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| \\
--- a/doc-src/IsarImplementation/Thy/logic.thy Thu Nov 20 22:39:12 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/logic.thy Fri Nov 21 07:34:36 2008 +0100
@@ -328,7 +328,7 @@
@{index_ML betapply: "term * term -> term"} \\
@{index_ML Sign.declare_const: "Properties.T -> (Name.binding * typ) * mixfix ->
theory -> term * theory"} \\
- @{index_ML Sign.add_abbrev: "string -> Properties.T -> bstring * term ->
+ @{index_ML Sign.add_abbrev: "string -> Properties.T -> Name.binding * term ->
theory -> (term * term) * theory"} \\
@{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
@{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\