--- a/doc-src/IsarImplementation/Thy/ML.thy Fri Nov 12 15:56:11 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Fri Nov 12 17:44:03 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 15:56:11 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Fri Nov 12 17:44:03 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%
%
--- a/src/Pure/General/symbol.ML Fri Nov 12 15:56:11 2010 +0100
+++ b/src/Pure/General/symbol.ML Fri Nov 12 17:44:03 2010 +0100
@@ -6,7 +6,7 @@
signature SYMBOL =
sig
- type symbol
+ type symbol = string
val SOH: symbol
val STX: symbol
val ENQ: symbol
--- a/src/Pure/library.ML Fri Nov 12 15:56:11 2010 +0100
+++ b/src/Pure/library.ML Fri Nov 12 17:44:03 2010 +0100
@@ -210,12 +210,12 @@
val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
val gensym: string -> string
- type stamp
+ type stamp = unit Unsynchronized.ref
val stamp: unit -> stamp
- type serial
+ type serial = int
val serial: unit -> serial
val serial_string: unit -> string
- structure Object: sig type T end
+ structure Object: sig type T = exn end
end;
signature LIBRARY =