# HG changeset patch
# User haftmann
# Date 1232611496 -3600
# Node ID 24a58ae5dc0e4879e86931b18d01be711160f2af
# Parent  1f7b1b0df292c2eaf8c304e249504d7e3dbefc74
binding replaces bstring

diff -r 1f7b1b0df292 -r 24a58ae5dc0e doc-src/IsarImplementation/Thy/document/logic.tex
--- a/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Jan 22 09:04:46 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Jan 22 09:04:56 2009 +0100
@@ -594,9 +594,9 @@
 \verb|  -> (string * ('a -> thm)) * theory| \\
   \end{mldecls}
   \begin{mldecls}
-  \indexml{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (string * term) list -> theory -> theory| \\
+  \indexml{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (binding * term) list -> theory -> theory| \\
   \indexml{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
-  \indexml{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory| \\
+  \indexml{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory| \\
   \end{mldecls}
 
   \begin{description}
diff -r 1f7b1b0df292 -r 24a58ae5dc0e doc-src/IsarImplementation/Thy/logic.thy
--- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Jan 22 09:04:46 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Jan 22 09:04:56 2009 +0100
@@ -596,9 +596,9 @@
   -> (string * ('a -> thm)) * theory"} \\
   \end{mldecls}
   \begin{mldecls}
-  @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
+  @{index_ML Theory.add_axioms_i: "(binding * term) list -> theory -> theory"} \\
   @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
-  @{index_ML Theory.add_defs_i: "bool -> bool -> (bstring * term) list -> theory -> theory"} \\
+  @{index_ML Theory.add_defs_i: "bool -> bool -> (binding * term) list -> theory -> theory"} \\
   \end{mldecls}
 
   \begin{description}