1.1 --- a/src/Tools/isac/calcelems.sml	Mon Sep 13 16:36:14 2010 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Mon Sep 13 17:21:22 2010 +0200
     1.3 @@ -336,11 +336,11 @@
     1.4    | ketype2str' Met_ = "Method";
     1.5  
     1.6  (*see 'How to manage theorys in subproblems' at 'type thyID'*)
     1.7 -val theory'  = ref ([]:(theory' * theory) list);
     1.8 +val theory'  = Unsynchronized.ref ([]:(theory' * theory) list);
     1.9  
    1.10  (*.all theories defined for Scripts, recorded in Scripts/Script.ML; 
    1.11     in order to distinguish them from general IsacKnowledge defined later on.*)
    1.12 -val script_thys = ref ([] : (theory' * theory) list);
    1.13 +val script_thys = Unsynchronized.ref ([] : (theory' * theory) list);
    1.14  
    1.15  
    1.16  (*rewrite orders, also stored in 'type met' and type 'and rls'
    1.17 @@ -359,10 +359,10 @@
    1.18  (*WN060120 a hack to get alltogether run again with minimal effort:
    1.19    theory' is inserted for creating thy_hierarchy; calls for assoc_rls
    1.20    need not be called*)
    1.21 -val ruleset' = ref ([]:(rls' * (theory' * rls)) list);
    1.22 +val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list);
    1.23  
    1.24  (*FIXME.040207 calclist': used by prep_rls, NOT in met*)
    1.25 -val calclist'= ref ([]: calc list);
    1.26 +val calclist'= Unsynchronized.ref ([]: calc list);
    1.27  
    1.28  (*.the hierarchy of thydata.*)
    1.29  
    1.30 @@ -403,10 +403,10 @@
    1.31  val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
    1.32  
    1.33  type thehier = (thydata ptyp) list;
    1.34 -val thehier = ref ([] : thehier);
    1.35 +val thehier = Unsynchronized.ref ([] : thehier);
    1.36  
    1.37  (*.an association list, gets the value once in Isac.ML.*)
    1.38 -val isab_thm_thy = ref ([] : (thmID * (thyID * term)) list);
    1.39 +val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list);
    1.40  
    1.41  
    1.42  type path = string;
    1.43 @@ -632,18 +632,18 @@
    1.44  
    1.45  
    1.46  (*.trace internal steps of isac's rewriter*)
    1.47 -val trace_rewrite = ref false;
    1.48 +val trace_rewrite = Unsynchronized.ref false;
    1.49  (*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
    1.50 -val depth = ref 99999;
    1.51 +val depth = Unsynchronized.ref 99999;
    1.52  (*.no of rewrites exceeding this int -> NO rewrite.*)
    1.53  (*WN060829 still unused...*)
    1.54 -val lim_rewrite = ref 99999;
    1.55 +val lim_rewrite = Unsynchronized.ref 99999;
    1.56  (*.no of derivation-elements exceeding this int -> SOME derivation-elements.*)
    1.57 -val lim_deriv = ref 100;
    1.58 +val lim_deriv = Unsynchronized.ref 100;
    1.59  (*.switch for checking guhs unique before storing a pbl or met;
    1.60     set true at startup (done at begin of ROOT.ML)
    1.61     set false for editing IsacKnowledge (done at end of ROOT.ML).*)
    1.62 -val check_guhs_unique = ref false;
    1.63 +val check_guhs_unique = Unsynchronized.ref false;
    1.64  
    1.65  
    1.66  datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)