# HG changeset patch
# User wenzelm
# Date 1206567597 -3600
# Node ID 1ceabad5a2c8f79fb5ad8e8fe5da0b71459bb9a9
# Parent  6964c4799f470b25e60d53fd32d3f5cebc9cb5e4
renamed ML_Context.>> to Context.>> (again);

diff -r 6964c4799f47 -r 1ceabad5a2c8 doc-src/IsarImplementation/Thy/integration.thy
--- a/doc-src/IsarImplementation/Thy/integration.thy	Wed Mar 26 22:38:55 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/integration.thy	Wed Mar 26 22:39:57 2008 +0100
@@ -241,7 +241,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML the_context: "unit -> theory"} \\
-  @{index_ML "ML_Context.>> ": "(theory -> theory) -> unit"} \\
+  @{index_ML "Context.>> ": "(theory -> theory) -> unit"} \\
   \end{mldecls}
 
   \begin{description}
@@ -255,7 +255,7 @@
   information immediately, or produce an explicit @{ML_type
   theory_ref} (cf.\ \secref{sec:context-theory}).
 
-  \item @{ML "ML_Context.>>"}~@{text f} applies theory transformation
+  \item @{ML "Context.>>"}~@{text f} applies theory transformation
   @{text f} to the current theory of the {\ML} toplevel.  In order to
   work as expected, the theory should be still under construction, and
   the Isar language element that invoked the {\ML} compiler in the