diff -r 070d539ba403 -r ab6f04807005 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Tue Jul 31 19:26:35 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Tue Jul 31 19:38:33 2007 +0200
@@ -165,8 +165,8 @@
 
   Any user-code that works relatively to the present background theory
   is already safe.  Contextual data may be easily stored within the
-  theory or proof context, thanks to the generic context data concept
-  of Isabelle/Isar (see \secref{sec:context-data}).  This greatly
+  theory or proof context, thanks to the generic data concept of
+  Isabelle/Isar (see \secref{sec:context-data}).  This greatly
   diminishes the demand for global state information in the first
   place.
 
@@ -194,10 +194,10 @@
   values, without any special precautions for multithreading.  Apart
   from the fully general functors for theory and proof data (see
   \secref{sec:context-data}) there are drop-in replacements that
-  emulate primitive references for the most basic cases of
-  \emph{configuration options} for type @{ML_type "bool"}/@{ML_type
-  "int"}/@{ML_type "string"} (see structure @{ML_struct ConfigOption})
-  and lists of theorems (see functor @{ML_functor NamedThmsFun}).
+  emulate primitive references for common cases of \emph{configuration
+  options} for type @{ML_type "bool"}/@{ML_type "int"}/@{ML_type
+  "string"} (see structure @{ML_struct ConfigOption}) and lists of
+  theorems (see functor @{ML_functor NamedThmsFun}).
 
   \item Keep components with local state information
   \emph{re-entrant}.  Instead of poking initial values into (private)
@@ -214,15 +214,15 @@
   example is the @{ML show_types} flag, which tells the pretty printer
   to output explicit type information for terms.  Such flags usually
   do not affect the functionality of the core system, but only the
-  output being presented to the user.
+  view being presented to the user.
 
   Occasionally, such global process flags are treated like implicit
   arguments to certain operations, by using the @{ML setmp} combinator
-  for safe temporary assignment.  Traditionally its main purpose was
-  to ensure proper recovery of the original value when exceptions are
-  raised in the body.  Now the functionality is extended to enter the
-  \emph{critical section}, with its usual potential of degrading
-  parallelism.
+  for safe temporary assignment.  Its traditional purpose was to
+  ensure proper recovery of the original value when exceptions are
+  raised in the body, now the functionality is extended to enter the
+  \emph{critical section} (with its usual potential of degrading
+  parallelism).
 
   Note that recovery of plain value passing semantics via @{ML
   setmp}~@{text "ref value"} assumes that this @{text "ref"} is
@@ -247,10 +247,10 @@
 
   Recall that in an open ``LCF-style'' system like Isabelle/Isar, the
   user participates in constructing the overall environment.  This
-  means that state-based facilities offered by one component need to
-  be used with caution later on.  Minimizing critical elements, by
-  staying within the plain value-oriented view relative to theory or
-  proof contexts most of the time, will also reduce the chance of
+  means that state-based facilities offered by one component will
+  require special caution later on.  So minimizing critical elements,
+  by staying within the plain value-oriented view relative to theory
+  or proof contexts most of the time, will also reduce the chance of
   mishaps occurring to end-users.
 *}
 
@@ -264,9 +264,10 @@
   \begin{description}
 
   \item @{ML NAMED_CRITICAL}~@{text "name f"} evaluates @{text "f ()"}
-  while staying within the critical section.  The @{text "name"}
-  argument serves for diagnostic output and might help to determine
-  sources of congestion.
+  while staying within the critical section of Isabelle/Isar.  No
+  other thread may do so at the same time, but non-critical parallel
+  execution will continue.  The @{text "name"} argument serves for
+  diagnostic purposes and might help to spot sources of congestion.
 
   \item @{ML CRITICAL} is the same as @{ML NAMED_CRITICAL} with empty
   name argument.