--- 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} *}
--- 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%
%