removed pointless trace msg.
authornipkow
Wed, 04 Jan 2006 16:37:57 +0100
changeset 18572 dab1dd61e59d
parent 18571 4927aa1feb23
child 18573 0ee7eab8c845
removed pointless trace msg.
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) =