# HG changeset patch
# User haftmann
# Date 1227249276 -3600
# Node ID 4fe0e90080ce6de8ab4b47c346d32b1dd36b9979
# Parent  3d9873c4c40903c293376baf6856de000d73038c
Name.binding

diff -r 3d9873c4c409 -r 4fe0e90080ce doc-src/IsarImplementation/Thy/document/logic.tex
--- 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| \\
diff -r 3d9873c4c409 -r 4fe0e90080ce doc-src/IsarImplementation/Thy/logic.thy
--- 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"} \\