diff -r 7b4fb2a2c75e -r eea3c9048c7a doc-src/IsarImplementation/Thy/document/integration.tex
--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Sat Nov 04 19:25:39 2006 +0100
@@ -184,7 +184,7 @@
 \verb|  Toplevel.transition -> Toplevel.transition| \\
   \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
 \verb|  Toplevel.transition -> Toplevel.transition| \\
-  \indexml{Toplevel.proof-to-theory}\verb|Toplevel.proof_to_theory: (Proof.state -> theory) ->|\isasep\isanewline%
+  \indexml{Toplevel.end-proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
 \verb|  Toplevel.transition -> Toplevel.transition| \\
   \end{mldecls}
 
@@ -217,9 +217,9 @@
   command, with zero or more result states (represented as a lazy
   list).
 
-  \item \verb|Toplevel.proof_to_theory|~\isa{tr} adjoins a
-  concluding proof command, that returns the resulting theory, after
-  storing the resulting facts etc.
+  \item \verb|Toplevel.end_proof|~\isa{tr} adjoins a concluding
+  proof command, that returns the resulting theory, after storing the
+  resulting facts in the context etc.
 
   \end{description}%
 \end{isamarkuptext}%