# HG changeset patch
# User nipkow
# Date 1136389077 -3600
# Node ID dab1dd61e59da2b341db12390d671b6f26763648
# Parent  4927aa1feb232a819a9eb5fb1089b9ba046143d4
removed pointless trace msg.

diff -r 4927aa1feb23 -r dab1dd61e59d src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Jan 04 16:14:15 2006 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Jan 04 16:37:57 2006 +0100
@@ -548,11 +548,7 @@
                        else (replicate n Rat.zero,hist)
        in warning "arith failed - see trace for a counter example";
           print_ex ((map s_of_t atoms)~~discr) (findex discr start)
-          handle NoEx =>
-  (tracing "The decision procedure failed to prove your proposition\n\
-           \but could not construct a counter example either.\n\
-           \Probably the proposition is true but cannot be proved\n\
-           \by the incomplete decision procedure.")
+          handle NoEx => (tracing "Sorry, no counter example.")
        end;
 
 fun mknat pTs ixs (atom,i) =