# HG changeset patch
# User wenzelm
# Date 1289580243 -3600
# Node ID b41c6b5a7a35ee0175bff48e29cfcb8b7ae769e6
# Parent  516a367eb38cf311b281ad0e8224a0f185b6fe31# Parent  0bc83ae22789ef4ea64e3027712f9d30a307f545
merged

diff -r 516a367eb38c -r b41c6b5a7a35 doc-src/IsarImplementation/Thy/ML.thy
--- 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} *}
diff -r 516a367eb38c -r b41c6b5a7a35 doc-src/IsarImplementation/Thy/document/ML.tex
--- 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%
 %
diff -r 516a367eb38c -r b41c6b5a7a35 src/Pure/General/symbol.ML
--- 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
diff -r 516a367eb38c -r b41c6b5a7a35 src/Pure/library.ML
--- 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 =