--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon May 03 14:25:56 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon May 03 14:31:33 2010 +0200
@@ -282,7 +282,7 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{Proof.context}\verb|type Proof.context| \\
- \indexdef{}{ML}{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
+ \indexdef{}{ML}{ProofContext.init\_global}\verb|ProofContext.init_global: theory -> Proof.context| \\
\indexdef{}{ML}{ProofContext.theory\_of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
\indexdef{}{ML}{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
\end{mldecls}
@@ -293,7 +293,7 @@
of this type are essentially pure values, with a sliding reference
to the background theory.
- \item \verb|ProofContext.init|~\isa{thy} produces a proof context
+ \item \verb|ProofContext.init_global|~\isa{thy} produces a proof context
derived from \isa{thy}, initializing all data.
\item \verb|ProofContext.theory_of|~\isa{ctxt} selects the
@@ -355,7 +355,7 @@
theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required.
\item \verb|Context.proof_of|~\isa{context} always produces a
- proof context from the generic \isa{context}, using \verb|ProofContext.init| as required (note that this re-initializes the
+ proof context from the generic \isa{context}, using \verb|ProofContext.init_global| as required (note that this re-initializes the
context data with each invocation).
\end{description}%