less verbose SAT tactic

--- a/src/HOL/Tools/sat.ML	Thu May 01 22:57:34 2014 +0200
+++ b/src/HOL/Tools/sat.ML	Thu May 01 22:57:36 2014 +0200
@@ -332,8 +332,10 @@
       end
   in
     case
-      let val the_solver = Config.get ctxt solver
-      in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end
+      let
+        val the_solver = Config.get ctxt solver
+        val _ = cond_tracing ctxt (fn () => "Invoking solver " ^ the_solver)
+      in SatSolver.invoke_solver the_solver fm end
     of
       SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) =>
        (cond_tracing ctxt (fn () =>