# HG changeset patch
# User nipkow
# Date 1391947643 -3600
# Node ID 5e5c36b051af516ebfacd7246fb8816836490658
# Parent  d459a63ca42f12147443fa3e64e30b012aad8d61
disabled counterexample output for now; confusing because often incorrect

diff -r d459a63ca42f -r 5e5c36b051af src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Sat Feb 08 20:34:10 2014 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sun Feb 09 13:07:23 2014 +0100
@@ -763,7 +763,7 @@
                         (Name.invent (Variable.names_of ctxt') Name.uu (length Ts - length params))
                       val params' = (more_names @ param_names) ~~ Ts
                     in
-                      trace_ex ctxt'' params' atoms (discr initems) n hist
+                      () (*trace_ex ctxt'' params' atoms (discr initems) n hist*)
                     end; NONE)
           end
       | refute [] js = SOME js