# HG changeset patch
# User boehmes
# Date 1269254709 -3600
# Node ID 9b579860d59b07312f16a7ebaf99f7f2688e75ee
# Parent  c93bda4fdf151bcc09806134801dfaf91d7ea038
removed warning_count (known causes for warnings have been resolved)

diff -r c93bda4fdf15 -r 9b579860d59b src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Mon Mar 22 10:38:28 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Mon Mar 22 11:45:09 2010 +0100
@@ -22,7 +22,6 @@
   val global_setup: theory -> theory
   val split_limit: int Config.T
   val neq_limit: int Config.T
-  val warning_count: int Unsynchronized.ref
   val trace: bool Unsynchronized.ref
 end;
 
@@ -797,7 +796,6 @@
 fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
 val lin_arith_tac = Fast_Arith.lin_arith_tac;
 val trace = Fast_Arith.trace;
-val warning_count = Fast_Arith.warning_count;
 
 (* reduce contradictory <= to False.
    Most of the work is done by the cancel tactics. *)
diff -r c93bda4fdf15 -r 9b579860d59b src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Mon Mar 22 10:38:28 2010 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Mar 22 11:45:09 2010 +0100
@@ -96,7 +96,6 @@
                      number_of : serial * (theory -> typ -> int -> cterm)})
                 -> Context.generic -> Context.generic
   val trace: bool Unsynchronized.ref
-  val warning_count: int Unsynchronized.ref;
 end;
 
 functor Fast_Lin_Arith
@@ -426,9 +425,6 @@
 fun trace_msg msg =
   if !trace then tracing msg else ();
 
-val warning_count = Unsynchronized.ref 0;
-val warning_count_max = 10;
-
 val union_term = union Pattern.aeconv;
 val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'));
 
@@ -532,17 +528,11 @@
       val _ =
         if LA_Logic.is_False fls then ()
         else
-          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, ""] @
-                 (if count <> warning_count_max then []
-                  else ["\n(Reached maximal message count -- disabling future warnings)"])));
-                warning "Linear arithmetic should have refuted the assumptions.\n\
-                  \Please inform Tobias Nipkow.")
-          end;
+         (tracing (cat_lines
+           (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
+            ["Proved:", Display.string_of_thm ctxt fls, ""]));
+          warning "Linear arithmetic should have refuted the assumptions.\n\
+            \Please inform Tobias Nipkow.")
     in fls end
     handle FalseE thm => trace_thm ctxt "False reached early:" thm
   end;