--- a/doc-src/IsarImplementation/Thy/Prelim.thy Sun Aug 26 22:23:10 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Sun Aug 26 22:32:22 2012 +0200
@@ -157,7 +157,7 @@
@{index_ML Theory.checkpoint: "theory -> theory"} \\
@{index_ML Theory.copy: "theory -> theory"} \\
@{index_ML Theory.merge: "theory * theory -> theory"} \\
- @{index_ML Theory.begin_theory: "string -> theory list -> theory"} \\
+ @{index_ML Theory.begin_theory: "string * Position.T -> theory list -> theory"} \\
@{index_ML Theory.parents_of: "theory -> theory list"} \\
@{index_ML Theory.ancestors_of: "theory -> theory list"} \\
\end{mldecls}
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Sun Aug 26 22:23:10 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Sun Aug 26 22:32:22 2012 +0200
@@ -183,7 +183,7 @@
\indexdef{}{ML}{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
\indexdef{}{ML}{Theory.copy}\verb|Theory.copy: theory -> theory| \\
\indexdef{}{ML}{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
- \indexdef{}{ML}{Theory.begin\_theory}\verb|Theory.begin_theory: string -> theory list -> theory| \\
+ \indexdef{}{ML}{Theory.begin\_theory}\verb|Theory.begin_theory: string * Position.T -> theory list -> theory| \\
\indexdef{}{ML}{Theory.parents\_of}\verb|Theory.parents_of: theory -> theory list| \\
\indexdef{}{ML}{Theory.ancestors\_of}\verb|Theory.ancestors_of: theory -> theory list| \\
\end{mldecls}