diff -r 30e7321dfa50 -r 16d56796f5a0 src/Tools/isac/calcelems.sml
--- a/src/Tools/isac/calcelems.sml	Mon Sep 13 16:36:14 2010 +0200
+++ b/src/Tools/isac/calcelems.sml	Mon Sep 13 17:21:22 2010 +0200
@@ -336,11 +336,11 @@
   | ketype2str' Met_ = "Method";
 
 (*see 'How to manage theorys in subproblems' at 'type thyID'*)
-val theory'  = ref ([]:(theory' * theory) list);
+val theory'  = Unsynchronized.ref ([]:(theory' * theory) list);
 
 (*.all theories defined for Scripts, recorded in Scripts/Script.ML; 
    in order to distinguish them from general IsacKnowledge defined later on.*)
-val script_thys = ref ([] : (theory' * theory) list);
+val script_thys = Unsynchronized.ref ([] : (theory' * theory) list);
 
 
 (*rewrite orders, also stored in 'type met' and type 'and rls'
@@ -359,10 +359,10 @@
 (*WN060120 a hack to get alltogether run again with minimal effort:
   theory' is inserted for creating thy_hierarchy; calls for assoc_rls
   need not be called*)
-val ruleset' = ref ([]:(rls' * (theory' * rls)) list);
+val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list);
 
 (*FIXME.040207 calclist': used by prep_rls, NOT in met*)
-val calclist'= ref ([]: calc list);
+val calclist'= Unsynchronized.ref ([]: calc list);
 
 (*.the hierarchy of thydata.*)
 
@@ -403,10 +403,10 @@
 val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
 
 type thehier = (thydata ptyp) list;
-val thehier = ref ([] : thehier);
+val thehier = Unsynchronized.ref ([] : thehier);
 
 (*.an association list, gets the value once in Isac.ML.*)
-val isab_thm_thy = ref ([] : (thmID * (thyID * term)) list);
+val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list);
 
 
 type path = string;
@@ -632,18 +632,18 @@
 
 
 (*.trace internal steps of isac's rewriter*)
-val trace_rewrite = ref false;
+val trace_rewrite = Unsynchronized.ref false;
 (*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
-val depth = ref 99999;
+val depth = Unsynchronized.ref 99999;
 (*.no of rewrites exceeding this int -> NO rewrite.*)
 (*WN060829 still unused...*)
-val lim_rewrite = ref 99999;
+val lim_rewrite = Unsynchronized.ref 99999;
 (*.no of derivation-elements exceeding this int -> SOME derivation-elements.*)
-val lim_deriv = ref 100;
+val lim_deriv = Unsynchronized.ref 100;
 (*.switch for checking guhs unique before storing a pbl or met;
    set true at startup (done at begin of ROOT.ML)
    set false for editing IsacKnowledge (done at end of ROOT.ML).*)
-val check_guhs_unique = ref false;
+val check_guhs_unique = Unsynchronized.ref false;
 
 
 datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)