src/Provers/Arith/fast_lin_arith.ML

                  lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}
                  -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
                      lessD: thm list, neqE: thm list, simpset: Simplifier.simpset})
                 -> Context.generic -> Context.generic
   val trace: bool ref
+  val warning_count: int ref;
   val cut_lin_arith_tac: simpset -> int -> tactic
   val lin_arith_tac: Proof.context -> bool -> int -> tactic
   val lin_arith_simproc: simpset -> term -> thm option
 end;
 

   (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_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')));
 
 (* FIXME OPTIMIZE!!!! (partly done already)

 with 0 <= n.
 *)
 local
   exception FalseE of thm
 in
+
 fun mkthm ss asms (just: injust) =
   let
     val ctxt = Simplifier.the_context ss;
     val thy = ProofContext.theory_of ctxt;
     val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = get_data ctxt;

         | mk (NotLessD j)         = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
         | mk (Added (j1, j2))     = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
         | mk (Multiplied (n, j))  = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (multn (n, mk j)))
         | mk (Multiplied2 (n, j)) = simp (trace_msg ("**" ^ string_of_int n); trace_thm "**" (multn2 (n, mk j)))
 
-  in trace_msg "mkthm";
-     let val thm = trace_thm "Final thm:" (mk just)
-     in let val fls = simplify simpset' thm
-        in trace_thm "After simplification:" fls;
-           if LA_Logic.is_False fls then fls
-           else
-            (tracing "Assumptions:"; List.app (tracing o Display.string_of_thm) asms;
-             tracing "Proved:"; tracing (Display.string_of_thm fls);
-             warning "Linear arithmetic should have refuted the assumptions.\n\
-                     \Please inform Tobias Nipkow ([e-mail]).";
-             fls)
-        end
-     end handle FalseE thm => trace_thm "False reached early:" thm
-  end
+  in
+    let
+      val _ = trace_msg "mkthm";
+      val thm = trace_thm "Final thm:" (mk just);
+      val fls = simplify simpset' thm;
+      val _ = trace_thm "After simplification:" fls;
+      val _ =
+        if LA_Logic.is_False fls then ()
+        else
+          let val count = CRITICAL (fn () => inc warning_count) in
+            if count > warning_count_max then ()
+            else
+              (tracing (cat_lines
+                (["Assumptions:"] @ map Display.string_of_thm asms @ [""] @
+                 ["Proved:", Display.string_of_thm 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 ([e-mail]).")
+          end;
+    in fls end
+    handle FalseE thm => trace_thm "False reached early:" thm
+  end;
+
 end;
 
 fun coeff poly atom =
   AList.lookup Pattern.aeconv poly atom |> the_default 0;