replaced Toplevel.proof_to_theory by Toplevel.end_proof;

--- a/doc-src/IsarImplementation/Thy/integration.thy	Sat Nov 04 12:53:35 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/integration.thy	Sat Nov 04 13:19:04 2006 +0100
@@ -141,7 +141,7 @@
   Toplevel.transition -> Toplevel.transition"} \\
   @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.seq) ->
   Toplevel.transition -> Toplevel.transition"} \\
-  @{index_ML Toplevel.proof_to_theory: "(Proof.state -> theory) ->
+  @{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) ->
   Toplevel.transition -> Toplevel.transition"} \\
   \end{mldecls}
 
@@ -174,9 +174,9 @@
   command, with zero or more result states (represented as a lazy
   list).
 
-  \item @{ML Toplevel.proof_to_theory}~@{text "tr"} adjoins a
-  concluding proof command, that returns the resulting theory, after
-  storing the resulting facts etc.
+  \item @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding
+  proof command, that returns the resulting theory, after storing the
+  resulting facts in the context etc.
 
   \end{description}
 *}