# HG changeset patch
# User blanchet
# Date 1260182689 -3600
# Node ID ef2776c8979986438046a57587a126564c79b266
# Parent  5426ada71790723e0a5e879e39a396440d471ea1
better error message in Refute when specifying a non-existing SAT solver

diff -r 5426ada71790 -r ef2776c89799 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Mon Dec 07 09:35:18 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Mon Dec 07 11:44:49 2009 +0100
@@ -1192,9 +1192,15 @@
         val fm_u  = (if negate then toFalse else toTrue) (hd intrs)
         val fm_ax = PropLogic.all (map toTrue (tl intrs))
         val fm    = PropLogic.all [#wellformed args, fm_ax, fm_u]
+        val solver =
+          SatSolver.invoke_solver satsolver
+          handle Option.Option =>
+                 error ("Unknown SAT solver: " ^ quote satsolver ^
+                        ". Available solvers: " ^
+                        commas (map (quote o fst) (!SatSolver.solvers)) ^ ".")
       in
         priority "Invoking SAT solver...";
-        (case SatSolver.invoke_solver satsolver fm of
+        (case solver fm of
           SatSolver.SATISFIABLE assignment =>
           (priority ("*** Model found: ***\n" ^ print_model thy model
             (fn i => case assignment i of SOME b => b | NONE => true));