--- a/src/Doc/Implementation/ML.thy Tue Apr 05 19:41:58 2016 +0200
+++ b/src/Doc/Implementation/ML.thy Tue Apr 05 20:03:24 2016 +0200
@@ -616,15 +616,15 @@
text %mlref \<open>
\begin{mldecls}
- @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
+ @{index_ML Context.the_generic_context: "unit -> Context.generic"} \\
@{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\
@{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\
@{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\
\end{mldecls}
- \<^descr> @{ML "ML_Context.the_generic_context ()"} refers to the theory context of
+ \<^descr> @{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
+ @{ML "Context.the_generic_context ()"} correctly. Recall that evaluation
of a function body is delayed until actual run-time.
\<^descr> @{ML "Context.>>"}~\<open>f\<close> applies context transformation \<open>f\<close> to the implicit