--- 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}
--- 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}