doc-src/IsarImplementation/Thy/integration.thy

   Toplevel.transition -> Toplevel.transition"} \\
   @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) ->
   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}
 
   \begin{description}
 

 
   \item @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof
   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}
 *}