1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Mon Mar 22 10:38:28 2010 +0100
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Mar 22 11:45:09 2010 +0100
     1.3 @@ -96,7 +96,6 @@
     1.4                       number_of : serial * (theory -> typ -> int -> cterm)})
     1.5                  -> Context.generic -> Context.generic
     1.6    val trace: bool Unsynchronized.ref
     1.7 -  val warning_count: int Unsynchronized.ref;
     1.8  end;
     1.9  
    1.10  functor Fast_Lin_Arith
    1.11 @@ -426,9 +425,6 @@
    1.12  fun trace_msg msg =
    1.13    if !trace then tracing msg else ();
    1.14  
    1.15 -val warning_count = Unsynchronized.ref 0;
    1.16 -val warning_count_max = 10;
    1.17 -
    1.18  val union_term = union Pattern.aeconv;
    1.19  val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'));
    1.20  
    1.21 @@ -532,17 +528,11 @@
    1.22        val _ =
    1.23          if LA_Logic.is_False fls then ()
    1.24          else
    1.25 -          let val count = CRITICAL (fn () => Unsynchronized.inc warning_count) in
    1.26 -            if count > warning_count_max then ()
    1.27 -            else
    1.28 -              (tracing (cat_lines
    1.29 -                (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
    1.30 -                 ["Proved:", Display.string_of_thm ctxt fls, ""] @
    1.31 -                 (if count <> warning_count_max then []
    1.32 -                  else ["\n(Reached maximal message count -- disabling future warnings)"])));
    1.33 -                warning "Linear arithmetic should have refuted the assumptions.\n\
    1.34 -                  \Please inform Tobias Nipkow.")
    1.35 -          end;
    1.36 +         (tracing (cat_lines
    1.37 +           (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
    1.38 +            ["Proved:", Display.string_of_thm ctxt fls, ""]));
    1.39 +          warning "Linear arithmetic should have refuted the assumptions.\n\
    1.40 +            \Please inform Tobias Nipkow.")
    1.41      in fls end
    1.42      handle FalseE thm => trace_thm ctxt "False reached early:" thm
    1.43    end;