# HG changeset patch
# User blanchet
# Date 1260184875 -3600
# Node ID 549855d22044e537ff9b8ed3e308806dbb367a16
# Parent  f215f52b7ff17509294ac012a864ecd53c4235a6# Parent  39f21f7bad7e26c8f48e1365f1d18f142002e04c
merged

diff -r f215f52b7ff1 -r 549855d22044 src/HOL/Refute.thy
--- 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
diff -r f215f52b7ff1 -r 549855d22044 src/HOL/Tools/refute.ML
--- 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));