# HG changeset patch
# User wenzelm
# Date 1346013142 -7200
# Node ID 10b89c1271532bd5947e2782d3a72d159a0e2a26
# Parent  05d4e5f660aefce08a6300a619d0c5e514f473c3
updated Theory.begin_theory;

diff -r 05d4e5f660ae -r 10b89c127153 doc-src/IsarImplementation/Thy/Prelim.thy
--- 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}
diff -r 05d4e5f660ae -r 10b89c127153 doc-src/IsarImplementation/Thy/document/Prelim.tex
--- 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}