# 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.