merged

--- a/src/HOL/Refute.thy	Mon Dec 07 11:18:44 2009 +0100
+++ b/src/HOL/Refute.thy	Mon Dec 07 12:21:15 2009 +0100
@@ -10,8 +10,6 @@
 theory Refute
 imports Hilbert_Choice List
 uses
-  "Tools/prop_logic.ML"
-  "Tools/sat_solver.ML"
   "Tools/refute.ML"
   "Tools/refute_isar.ML"
 begin

--- a/src/HOL/Tools/refute.ML	Mon Dec 07 11:18:44 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Mon Dec 07 12:21:15 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));