1.1 --- a/src/HOL/Tools/lin_arith.ML	Mon Mar 22 10:38:28 2010 +0100
     1.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon Mar 22 11:45:09 2010 +0100
     1.3 @@ -22,7 +22,6 @@
     1.4    val global_setup: theory -> theory
     1.5    val split_limit: int Config.T
     1.6    val neq_limit: int Config.T
     1.7 -  val warning_count: int Unsynchronized.ref
     1.8    val trace: bool Unsynchronized.ref
     1.9  end;
    1.10  
    1.11 @@ -797,7 +796,6 @@
    1.12  fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
    1.13  val lin_arith_tac = Fast_Arith.lin_arith_tac;
    1.14  val trace = Fast_Arith.trace;
    1.15 -val warning_count = Fast_Arith.warning_count;
    1.16  
    1.17  (* reduce contradictory <= to False.
    1.18     Most of the work is done by the cancel tactics. *)

     2.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Mon Mar 22 10:38:28 2010 +0100
     2.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Mar 22 11:45:09 2010 +0100
     2.3 @@ -96,7 +96,6 @@
     2.4                       number_of : serial * (theory -> typ -> int -> cterm)})
     2.5                  -> Context.generic -> Context.generic
     2.6    val trace: bool Unsynchronized.ref
     2.7 -  val warning_count: int Unsynchronized.ref;
     2.8  end;
     2.9  
    2.10  functor Fast_Lin_Arith
    2.11 @@ -426,9 +425,6 @@
    2.12  fun trace_msg msg =
    2.13    if !trace then tracing msg else ();
    2.14  
    2.15 -val warning_count = Unsynchronized.ref 0;
    2.16 -val warning_count_max = 10;
    2.17 -
    2.18  val union_term = union Pattern.aeconv;
    2.19  val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'));
    2.20  
    2.21 @@ -532,17 +528,11 @@
    2.22        val _ =
    2.23          if LA_Logic.is_False fls then ()
    2.24          else
    2.25 -          let val count = CRITICAL (fn () => Unsynchronized.inc warning_count) in
    2.26 -            if count > warning_count_max then ()
    2.27 -            else
    2.28 -              (tracing (cat_lines
    2.29 -                (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
    2.30 -                 ["Proved:", Display.string_of_thm ctxt fls, ""] @
    2.31 -                 (if count <> warning_count_max then []
    2.32 -                  else ["\n(Reached maximal message count -- disabling future warnings)"])));
    2.33 -                warning "Linear arithmetic should have refuted the assumptions.\n\
    2.34 -                  \Please inform Tobias Nipkow.")
    2.35 -          end;
    2.36 +         (tracing (cat_lines
    2.37 +           (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
    2.38 +            ["Proved:", Display.string_of_thm ctxt fls, ""]));
    2.39 +          warning "Linear arithmetic should have refuted the assumptions.\n\
    2.40 +            \Please inform Tobias Nipkow.")
    2.41      in fls end
    2.42      handle FalseE thm => trace_thm ctxt "False reached early:" thm
    2.43    end;