author | blanchet |
Thu, 29 Oct 2009 15:23:25 +0100 | |
changeset 33570 | 14f2880e7ccf |
parent 33569 | 1ebb8b7b9f6a |
child 33571 | 3655e51f9958 |
--- 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