doc-src/IsarImplementation/Thy/document/Prelim.tex

 \isatagmlref
 %
 \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}
 
   \begin{description}
 
   \item \verb|Proof.context| represents proof contexts.  Elements
   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
   background theory from \isa{ctxt}, dereferencing its internal
   \verb|theory_ref|.

 
   \item \verb|Context.theory_of|~\isa{context} always produces a
   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}%
 \end{isamarkuptext}%
 \isamarkuptrue%