--- a/src/HOL/Tools/refute.ML Fri Mar 26 12:21:50 2004 +0100
+++ b/src/HOL/Tools/refute.ML Fri Mar 26 14:53:17 2004 +0100
@@ -466,9 +466,12 @@
std_output " invoking SAT solver...";
case SatSolver.invoke_solver satsolver fm of
None =>
+ (std_output (" error: SAT solver " ^ quote satsolver ^ " not configured.\n");
+ true)
+ | Some None =>
(std_output " no model found.\n";
false)
- | Some assignment =>
+ | Some (Some assignment) =>
(writeln ("\nModel found:\n" ^ print_model thy model assignment);
true)
)