solver "auto" does not reverse the list of solvers anymore
authorwebertj
Thu Sep 22 13:52:55 2005 +0200 (2005-09-22)
changeset 17581a50a53081808
parent 17580 78a286d696c1
child 17582 df49216dc592
solver "auto" does not reverse the list of solvers anymore
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Thu Sep 22 07:56:16 2005 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Thu Sep 22 13:52:55 2005 +0200
     1.3 @@ -528,13 +528,13 @@
     1.4  				(if name="dpll" orelse name="enumerate" then
     1.5  					warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
     1.6  				else
     1.7 -					());
     1.8 +					debug ("Using SAT solver " ^ quote name ^ "."));
     1.9  				(* apply 'solver' to 'fm' *)
    1.10  				solver fm
    1.11  					handle SatSolver.NOT_CONFIGURED => loop solvers
    1.12  			)
    1.13  	in
    1.14 -		loop (rev (!SatSolver.solvers))
    1.15 +		loop (!SatSolver.solvers)
    1.16  	end
    1.17  in
    1.18  	SatSolver.add_solver ("auto", auto_solver)