src/HOL/Tools/sat_solver.ML
changeset 14805 eff7b9df27e9
parent 14753 f40b45db8cf0
child 14965 7155b319eafa
--- a/src/HOL/Tools/sat_solver.ML	Wed May 26 14:57:06 2004 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Wed May 26 17:42:46 2004 +0200
@@ -369,8 +369,8 @@
 			if name="auto" then
 				None
 			else
-				((if name="dpll" then
-					warning ("Using SAT solver \"dpll\"; for better performance, consider using an external solver.")
+				((if name="dpll" orelse name="enumerate" then
+					warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
 				else
 					());
 				solver fm)) (rev (!SatSolver.solvers))