# HG changeset patch
# User wenzelm
# Date 1418912514 -3600
# Node ID ba2a326fc271ad778eafd4a1cf730933f28c0445
# Parent  0e304b1568a55eced262825dcf686d050a565723
avoid repeated access to global variable (101 times in Complex_Main), which is actually synchronized after e557a9ddee5f;

diff -r 0e304b1568a5 -r ba2a326fc271 src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Dec 17 16:51:29 2014 +0100
+++ b/src/Pure/context.ML	Thu Dec 18 15:21:54 2014 +0100
@@ -376,13 +376,14 @@
 
 val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Any.T) Datatab.table);
 
-fun invoke_init k =
-  (case Datatab.lookup (Synchronized.value kinds) k of
+fun invoke_init tab k =
+  (case Datatab.lookup tab k of
     SOME init => init
   | NONE => raise Fail "Invalid proof data identifier");
 
 fun init_data thy =
-  Datatab.map (fn k => fn _ => invoke_init k thy) (Synchronized.value kinds);
+  let val tab = Synchronized.value kinds
+  in Datatab.map (fn k => fn _ => invoke_init tab k thy) tab end;
 
 fun init_new_data data thy =
   Datatab.merge (K true) (data, init_data thy);
@@ -414,7 +415,10 @@
 fun get k dest prf =
   (case Datatab.lookup (data_of_proof prf) k of
     SOME x => x
-  | NONE => invoke_init k (Proof_Context.theory_of prf)) |> dest;  (*adhoc value for old theories*)
+  | NONE =>
+      (*adhoc value for old theories*)
+      invoke_init (Synchronized.value kinds) k (Proof_Context.theory_of prf))
+  |> dest;
 
 fun put k mk x = map_prf (Datatab.update (k, mk x));