src/Provers/Arith/fast_lin_arith.ML

                  number_of : serial * (theory -> typ -> int -> cterm)}
                  -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
                      lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
                      number_of : serial * (theory -> typ -> int -> cterm)})
                 -> Context.generic -> Context.generic
-  val trace: bool ref
-  val warning_count: int ref;
+  val trace: bool Unsynchronized.ref
+  val warning_count: int Unsynchronized.ref;
 end;
 
 functor Fast_Lin_Arith
   (structure LA_Logic: LIN_ARITH_LOGIC and LA_Data: LIN_ARITH_DATA): FAST_LIN_ARITH =
 struct

 (* possible optimizations:
    use (var,coeff) rep or vector rep  tp save space;
    treat non-negative atoms separately rather than adding 0 <= atom
 *)
 
-val trace = ref false;
+val trace = Unsynchronized.ref false;
 
 datatype lineq_type = Eq | Le | Lt;
 
 datatype injust = Asm of int
                 | Nat of int (* index of atom *)

   (if !trace then tracing (cat_lines [msg, Syntax.string_of_term ctxt t]) else (); t)
 
 fun trace_msg msg =
   if !trace then tracing msg else ();
 
-val warning_count = ref 0;
+val warning_count = Unsynchronized.ref 0;
 val warning_count_max = 10;
 
 val union_term = curry (gen_union Pattern.aeconv);
 val union_bterm = curry (gen_union
   (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t')));

       val fls = simplify simpset' thm;
       val _ = trace_thm ctxt "After simplification:" fls;
       val _ =
         if LA_Logic.is_False fls then ()
         else
-          let val count = CRITICAL (fn () => inc warning_count) in
+          let val count = CRITICAL (fn () => Unsynchronized.inc warning_count) in
             if count > warning_count_max then ()
             else
               (tracing (cat_lines
                 (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
                  ["Proved:", Display.string_of_thm ctxt fls, ""] @