# HG changeset patch
# User wenzelm
# Date 1248520553 -7200
# Node ID 4086cdd8dd704a251595ea6500f9a460ffb3b806
# Parent  005f9abae1e3a78d04ac9be76a53df65603ee2ae
ML_Context.the_generic_context;

diff -r 005f9abae1e3 -r 4086cdd8dd70 doc-src/IsarImplementation/Thy/Integration.thy
--- a/doc-src/IsarImplementation/Thy/Integration.thy	Sat Jul 25 12:43:45 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/Integration.thy	Sat Jul 25 13:15:53 2009 +0200
@@ -239,20 +239,20 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML the_context: "unit -> theory"} \\
+  @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
   @{index_ML "Context.>> ": "(Context.generic -> Context.generic) -> unit"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML "the_context ()"} refers to the theory context of the
-  {\ML} toplevel --- at compile time!  {\ML} code needs to take care
-  to refer to @{ML "the_context ()"} correctly.  Recall that
-  evaluation of a function body is delayed until actual runtime.
-  Moreover, persistent {\ML} toplevel bindings to an unfinished theory
-  should be avoided: code should either project out the desired
-  information immediately, or produce an explicit @{ML_type
-  theory_ref} (cf.\ \secref{sec:context-theory}).
+  \item @{ML "ML_Context.the_generic_context ()"} refers to the theory
+  context of the {\ML} toplevel --- at compile time!  {\ML} code needs
+  to take care to refer to @{ML "ML_Context.the_generic_context ()"}
+  correctly.  Recall that evaluation of a function body is delayed
+  until actual runtime.  Moreover, persistent {\ML} toplevel bindings
+  to an unfinished theory should be avoided: code should either
+  project out the desired information immediately, or produce an
+  explicit @{ML_type theory_ref} (cf.\ \secref{sec:context-theory}).
 
   \item @{ML "Context.>>"}~@{text f} applies context transformation
   @{text f} to the implicit context of the {\ML} toplevel.
diff -r 005f9abae1e3 -r 4086cdd8dd70 doc-src/IsarImplementation/Thy/document/Integration.tex
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex	Sat Jul 25 12:43:45 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex	Sat Jul 25 13:15:53 2009 +0200
@@ -300,19 +300,20 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexdef{}{ML}{the\_context}\verb|the_context: unit -> theory| \\
+  \indexdef{}{ML}{ML\_Context.the\_generic\_context}\verb|ML_Context.the_generic_context: unit -> Context.generic| \\
   \indexdef{}{ML}{Context.$>$$>$ }\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
   \end{mldecls}
 
   \begin{description}
 
-  \item \verb|the_context ()| refers to the theory context of the
-  {\ML} toplevel --- at compile time!  {\ML} code needs to take care
-  to refer to \verb|the_context ()| correctly.  Recall that
-  evaluation of a function body is delayed until actual runtime.
-  Moreover, persistent {\ML} toplevel bindings to an unfinished theory
-  should be avoided: code should either project out the desired
-  information immediately, or produce an explicit \verb|theory_ref| (cf.\ \secref{sec:context-theory}).
+  \item \verb|ML_Context.the_generic_context ()| refers to the theory
+  context of the {\ML} toplevel --- at compile time!  {\ML} code needs
+  to take care to refer to \verb|ML_Context.the_generic_context ()|
+  correctly.  Recall that evaluation of a function body is delayed
+  until actual runtime.  Moreover, persistent {\ML} toplevel bindings
+  to an unfinished theory should be avoided: code should either
+  project out the desired information immediately, or produce an
+  explicit \verb|theory_ref| (cf.\ \secref{sec:context-theory}).
 
   \item \verb|Context.>>|~\isa{f} applies context transformation
   \isa{f} to the implicit context of the {\ML} toplevel.