src/Pure/context.ML

  {empty: Object.T,
   copy: Object.T -> Object.T,
   extend: Object.T -> Object.T,
   merge: Pretty.pp -> Object.T * Object.T -> Object.T};
 
-val kinds = ref (Datatab.empty: kind Datatab.table);
+val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
 
 fun invoke f k =
   (case Datatab.lookup (! kinds) k of
     SOME kind => f kind
   | NONE => sys_error "Invalid theory data identifier");

 
 fun declare_theory_data empty copy extend merge =
   let
     val k = serial ();
     val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
-    val _ = CRITICAL (fn () => change kinds (Datatab.update (k, kind)));
+    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
   in k end;
 
 val copy_data = Datatab.map' invoke_copy;
 val extend_data = Datatab.map' invoke_extend;
 

 (** datatype theory **)
 
 datatype theory =
   Theory of
    (*identity*)
-   {self: theory ref option,      (*dynamic self reference -- follows theory changes*)
+   {self: theory Unsynchronized.ref option,  (*dynamic self reference -- follows theory changes*)
     draft: bool,                  (*draft mode -- linear destructive changes*)
     id: serial,                   (*identifier*)
     ids: unit Inttab.table} *     (*cumulative identifiers of non-drafts -- symbolic body content*)
    (*data*)
    Object.T Datatab.table *       (*body content*)

 (* staleness *)
 
 fun eq_id (i: int, j) = i = j;
 
 fun is_stale
-    (Theory ({self = SOME (ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
+    (Theory ({self =
+        SOME (Unsynchronized.ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
       not (eq_id (id, id'))
   | is_stale (Theory ({self = NONE, ...}, _, _, _)) = true;
 
 fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy)
   | vitalize (thy as Theory ({self = NONE, draft, id, ids}, data, ancestry, history)) =
       let
-        val r = ref thy;
+        val r = Unsynchronized.ref thy;
         val thy' = Theory (make_identity (SOME r) draft id ids, data, ancestry, history);
       in r := thy'; thy' end;
 
 
 (* draft mode *)

 
 (*theory_ref provides a safe way to store dynamic references to a
   theory in external data structures -- a plain theory value would
   become stale as the self reference moves on*)
 
-datatype theory_ref = TheoryRef of theory ref;
-
-fun deref (TheoryRef (ref thy)) = thy;
+datatype theory_ref = TheoryRef of theory Unsynchronized.ref;
+
+fun deref (TheoryRef (Unsynchronized.ref thy)) = thy;
 
 fun check_thy thy =  (*thread-safe version*)
   let val thy_ref = TheoryRef (the_self thy) in
     if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy)
     else thy_ref

 
 (* proof data kinds *)
 
 local
 
-val kinds = ref (Datatab.empty: (theory -> Object.T) Datatab.table);
+val kinds = Unsynchronized.ref (Datatab.empty: (theory -> Object.T) Datatab.table);
 
 fun invoke_init k =
   (case Datatab.lookup (! kinds) k of
     SOME init => init
   | NONE => sys_error "Invalid proof data identifier");

 struct
 
 fun declare init =
   let
     val k = serial ();
-    val _ = CRITICAL (fn () => change kinds (Datatab.update (k, init)));
+    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, init)));
   in k end;
 
 fun get k dest prf =
   dest (case Datatab.lookup (data_of_proof prf) k of
     SOME x => x