# HG changeset patch
# User webertj
# Date 1127389975 -7200
# Node ID a50a53081808512ea455373ac4500286a3bd21c3
# Parent  78a286d696c1be710cd04baeb3ef072f04594afc
solver "auto" does not reverse the list of solvers anymore

diff -r 78a286d696c1 -r a50a53081808 src/HOL/Tools/sat_solver.ML
--- 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)