doc-src/IsarImplementation/Thy/Integration.thy

   @{index_ML_type Toplevel.state} \\
   @{index_ML Toplevel.UNDEF: "exn"} \\
   @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
   @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
   @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
-  @{index_ML Toplevel.debug: "bool ref"} \\
-  @{index_ML Toplevel.timing: "bool ref"} \\
-  @{index_ML Toplevel.profiling: "int ref"} \\
+  @{index_ML Toplevel.debug: "bool Unsynchronized.ref"} \\
+  @{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\
+  @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\
   \end{mldecls}
 
   \begin{description}
 
   \item @{ML_type Toplevel.state} represents Isar toplevel states,

   a theory or proof (!), otherwise raises @{ML Toplevel.UNDEF}.
 
   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
   state if available, otherwise raises @{ML Toplevel.UNDEF}.
 
-  \item @{ML "set Toplevel.debug"} makes the toplevel print further
+  \item @{ML "Toplevel.debug := true"} makes the toplevel print further
   details about internal error conditions, exceptions being raised
   etc.
 
-  \item @{ML "set Toplevel.timing"} makes the toplevel print timing
+  \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
   information for each Isar command being executed.
 
   \item @{ML Toplevel.profiling}~@{verbatim ":="}~@{text "n"} controls
   low-level profiling of the underlying {\ML} runtime system.  For
   Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space