# HG changeset patch
# User wenzelm
# Date 1289567197 -3600
# Node ID 76894f9754400af31a17c1fc2e15f5242cd6cae7
# Parent  f9057eca82f197a06cfd6ec73e093cd6bdcaf35f
never open Unsynchronized;

diff -r f9057eca82f1 -r 76894f975440 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Fri Nov 12 12:57:02 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Fri Nov 12 14:06:37 2010 +0100
@@ -1476,7 +1476,13 @@
   mutability.  Existing operations @{ML "!"}  and @{ML "op :="} are
   unchanged, but should be used with special precautions, say in a
   strictly local situation that is guaranteed to be restricted to
-  sequential evaluation --- now and in the future.  *}
+  sequential evaluation --- now and in the future.
+
+  \begin{warn}
+  Never @{ML_text "open Unsynchronized"}, not even in a local scope!
+  Pretending that mutable state is no problem is a very bad idea.
+  \end{warn}
+*}
 
 
 section {* Thread-safe programming \label{sec:multi-threading} *}
diff -r f9057eca82f1 -r 76894f975440 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Fri Nov 12 12:57:02 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Fri Nov 12 14:06:37 2010 +0100
@@ -1965,7 +1965,12 @@
   mutability.  Existing operations \verb|!|  and \verb|op :=| are
   unchanged, but should be used with special precautions, say in a
   strictly local situation that is guaranteed to be restricted to
-  sequential evaluation --- now and in the future.%
+  sequential evaluation --- now and in the future.
+
+  \begin{warn}
+  Never \verb|open Unsynchronized|, not even in a local scope!
+  Pretending that mutable state is no problem is a very bad idea.
+  \end{warn}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %