# HG changeset patch
# User wenzelm
# Date 1162642744 -3600
# Node ID 0f869edd6cc1ce8894561cfc004e9a3086ed8ad5
# Parent  276dd93cfa97d08726a5bfd90d28a872e533738b
replaced Toplevel.proof_to_theory by Toplevel.end_proof;

diff -r 276dd93cfa97 -r 0f869edd6cc1 doc-src/IsarImplementation/Thy/integration.thy
--- 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}
 *}