src/Provers/Arith/fast_lin_arith.ML
changeset 32740 9dd0a2f83429
parent 32283 3bebc195c124
child 32952 aeb1e44fbc19
     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -96,8 +96,8 @@
     1.4                       lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
     1.5                       number_of : serial * (theory -> typ -> int -> cterm)})
     1.6                  -> Context.generic -> Context.generic
     1.7 -  val trace: bool ref
     1.8 -  val warning_count: int ref;
     1.9 +  val trace: bool Unsynchronized.ref
    1.10 +  val warning_count: int Unsynchronized.ref;
    1.11  end;
    1.12  
    1.13  functor Fast_Lin_Arith
    1.14 @@ -152,7 +152,7 @@
    1.15     treat non-negative atoms separately rather than adding 0 <= atom
    1.16  *)
    1.17  
    1.18 -val trace = ref false;
    1.19 +val trace = Unsynchronized.ref false;
    1.20  
    1.21  datatype lineq_type = Eq | Le | Lt;
    1.22  
    1.23 @@ -426,7 +426,7 @@
    1.24  fun trace_msg msg =
    1.25    if !trace then tracing msg else ();
    1.26  
    1.27 -val warning_count = ref 0;
    1.28 +val warning_count = Unsynchronized.ref 0;
    1.29  val warning_count_max = 10;
    1.30  
    1.31  val union_term = curry (gen_union Pattern.aeconv);
    1.32 @@ -533,7 +533,7 @@
    1.33        val _ =
    1.34          if LA_Logic.is_False fls then ()
    1.35          else
    1.36 -          let val count = CRITICAL (fn () => inc warning_count) in
    1.37 +          let val count = CRITICAL (fn () => Unsynchronized.inc warning_count) in
    1.38              if count > warning_count_max then ()
    1.39              else
    1.40                (tracing (cat_lines