# HG changeset patch
# User wenzelm
# Date 1287512402 -3600
# Node ID dd014982f4caa796c2984f502416b21d3c61be3e
# Parent  c269f6bd0a1f9c5736a86c187bc8aa5c8855ba82
tuned;

diff -r c269f6bd0a1f -r dd014982f4ca doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Tue Oct 19 19:16:27 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Tue Oct 19 19:20:02 2010 +0100
@@ -674,6 +674,7 @@
 
 text %mlref {*
   \begin{mldecls}
+  @{index_ML_type "'a Unsynchronized.ref"} \\
   @{index_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\
   @{index_ML "!": "'a Unsynchronized.ref -> 'a"} \\
   @{index_ML "op :=": "'a Unsynchronized.ref * 'a -> unit"} \\
@@ -691,10 +692,10 @@
   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.  *}
 
 
-section {* Thread-safe programming *}
+section {* Thread-safe programming \label{sec:multi-threading} *}
 
 text {* Multi-threaded execution has become an everyday reality in
   Isabelle since Poly/ML 5.2.1 and Isabelle2008.  Isabelle/ML provides