# HG changeset patch
# User blanchet
# Date 1256826205 -3600
# Node ID 14f2880e7ccf583a9f8f31aebf09acf94c6483ca
# Parent  1ebb8b7b9f6afe73f644922ef2c1a07677c2f96e
make "auto" SAT solver less verbose

diff -r 1ebb8b7b9f6a -r 14f2880e7ccf src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Thu Oct 29 15:16:54 2009 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Thu Oct 29 15:23:25 2009 +0100
@@ -546,7 +546,7 @@
         (if name="dpll" orelse name="enumerate" then
           warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
         else
-          tracing ("Using SAT solver " ^ quote name ^ "."));
+          ());
         (* apply 'solver' to 'fm' *)
         solver fm
           handle SatSolver.NOT_CONFIGURED => loop solvers