make "auto" SAT solver less verbose
authorblanchet
Thu, 29 Oct 2009 15:23:25 +0100
changeset 33570 14f2880e7ccf
parent 33569 1ebb8b7b9f6a
child 33571 3655e51f9958
make "auto" SAT solver less verbose
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