# HG changeset patch
# User webertj
# Date 1085586166 -7200
# Node ID eff7b9df27e98470848262791ec7d80e3458e865
# Parent  8de39d3e8eb6cd8b534ea4a7e6c77090f331b918
solver "auto" now issues a warning when it uses solver "enumerate"

diff -r 8de39d3e8eb6 -r eff7b9df27e9 src/HOL/Tools/sat_solver.ML
--- 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))