--- a/src/HOL/Tools/sat_solver.ML Thu Sep 22 07:56:16 2005 +0200
+++ b/src/HOL/Tools/sat_solver.ML Thu Sep 22 13:52:55 2005 +0200
@@ -528,13 +528,13 @@
(if name="dpll" orelse name="enumerate" then
warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
else
- ());
+ debug ("Using SAT solver " ^ quote name ^ "."));
(* apply 'solver' to 'fm' *)
solver fm
handle SatSolver.NOT_CONFIGURED => loop solvers
)
in
- loop (rev (!SatSolver.solvers))
+ loop (!SatSolver.solvers)
end
in
SatSolver.add_solver ("auto", auto_solver)