diff -r b59766bc66c9 -r 8911c5a8b078 doc-src/IsarImplementation/Thy/document/integration.tex
--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Tue Jan 10 19:36:59 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Wed Jan 11 00:11:02 2006 +0100
@@ -181,8 +181,6 @@
 \verb|  Toplevel.transition -> Toplevel.transition| \\
   \indexml{Toplevel.theory-to-proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
 \verb|  Toplevel.transition -> Toplevel.transition| \\
-  \indexml{Toplevel.theory-theory-to-proof}\verb|Toplevel.theory_theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
-\verb|  Toplevel.transition -> Toplevel.transition| \\
   \indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
 \verb|  Toplevel.transition -> Toplevel.transition| \\
   \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
@@ -205,13 +203,10 @@
   \item \verb|Toplevel.theory| adjoins a theory transformer.
 
   \item \verb|Toplevel.theory_to_proof| adjoins a global goal function,
-  which turns a theory into a proof state.  The theory must not be
-  changed here!  The generic Isar goal setup includes an argument that
-  specifies how to apply the proven result to the theory, when the
-  proof is finished.
-
-  \item \verb|Toplevel.theory_theory_to_proof| is like \verb|Toplevel.theory_to_proof|, but allows the initial theory to be
-  changed before entering proof state.
+  which turns a theory into a proof state.  The theory may be changed
+  before entering the proof; the generic Isar goal setup includes an
+  argument that specifies how to apply the proven result to the
+  theory, when the proof is finished.
 
   \item \verb|Toplevel.proof| adjoins a deterministic proof command,
   with a singleton result state.