1.1 --- a/src/Pure/context.ML	Wed Jul 06 20:14:13 2011 +0200
     1.2 +++ b/src/Pure/context.ML	Wed Jul 06 20:46:06 2011 +0200
     1.3 @@ -128,10 +128,10 @@
     1.4    extend: Object.T -> Object.T,
     1.5    merge: pretty -> Object.T * Object.T -> Object.T};
     1.6  
     1.7 -val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
     1.8 +val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
     1.9  
    1.10  fun invoke name f k x =
    1.11 -  (case Datatab.lookup (! kinds) k of
    1.12 +  (case Datatab.lookup (Synchronized.value kinds) k of
    1.13      SOME kind =>
    1.14        if ! timing andalso name <> "" then
    1.15          Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.str_of (#pos kind))
    1.16 @@ -149,7 +149,7 @@
    1.17    let
    1.18      val k = serial ();
    1.19      val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
    1.20 -    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
    1.21 +    val _ = Synchronized.change kinds (Datatab.update (k, kind));
    1.22    in k end;
    1.23  
    1.24  val extend_data = Datatab.map invoke_extend;
    1.25 @@ -475,15 +475,15 @@
    1.26  
    1.27  local
    1.28  
    1.29 -val kinds = Unsynchronized.ref (Datatab.empty: (theory -> Object.T) Datatab.table);
    1.30 +val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Object.T) Datatab.table);
    1.31  
    1.32  fun invoke_init k =
    1.33 -  (case Datatab.lookup (! kinds) k of
    1.34 +  (case Datatab.lookup (Synchronized.value kinds) k of
    1.35      SOME init => init
    1.36    | NONE => raise Fail "Invalid proof data identifier");
    1.37  
    1.38  fun init_data thy =
    1.39 -  Datatab.map (fn k => fn _ => invoke_init k thy) (! kinds);
    1.40 +  Datatab.map (fn k => fn _ => invoke_init k thy) (Synchronized.value kinds);
    1.41  
    1.42  fun init_new_data data thy =
    1.43    Datatab.merge (K true) (data, init_data thy);
    1.44 @@ -511,7 +511,7 @@
    1.45  fun declare init =
    1.46    let
    1.47      val k = serial ();
    1.48 -    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, init)));
    1.49 +    val _ = Synchronized.change kinds (Datatab.update (k, init));
    1.50    in k end;
    1.51  
    1.52  fun get k dest prf =