# HG changeset patch
# User wenzelm
# Date 1272889893 -7200
# Node ID b0c047d03208a920f033e7d1a0a6490d54801ee6
# Parent  bafd82950e2469a77bc880744fac9f3b7cad3b6a
ProofContext.init_global;

diff -r bafd82950e24 -r b0c047d03208 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Mon May 03 14:25:56 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Mon May 03 14:31:33 2010 +0200
@@ -243,7 +243,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML_type Proof.context} \\
-  @{index_ML ProofContext.init: "theory -> Proof.context"} \\
+  @{index_ML ProofContext.init_global: "theory -> Proof.context"} \\
   @{index_ML ProofContext.theory_of: "Proof.context -> theory"} \\
   @{index_ML ProofContext.transfer: "theory -> Proof.context -> Proof.context"} \\
   \end{mldecls}
@@ -254,7 +254,7 @@
   of this type are essentially pure values, with a sliding reference
   to the background theory.
 
-  \item @{ML ProofContext.init}~@{text "thy"} produces a proof context
+  \item @{ML ProofContext.init_global}~@{text "thy"} produces a proof context
   derived from @{text "thy"}, initializing all data.
 
   \item @{ML ProofContext.theory_of}~@{text "ctxt"} selects the
@@ -305,7 +305,7 @@
 
   \item @{ML Context.proof_of}~@{text "context"} always produces a
   proof context from the generic @{text "context"}, using @{ML
-  "ProofContext.init"} as required (note that this re-initializes the
+  "ProofContext.init_global"} as required (note that this re-initializes the
   context data with each invocation).
 
   \end{description}
diff -r bafd82950e24 -r b0c047d03208 doc-src/IsarImplementation/Thy/document/Prelim.tex
--- 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}%