# HG changeset patch
# User webertj
# Date 1080309197 -3600
# Node ID 863258b0cdcad3c6a1bcf1d5c27fe0f57585b279
# Parent  157d0ea7b2dac6ab2693ff9fe21f43788e570691
slightly different SAT solver interface

diff -r 157d0ea7b2da -r 863258b0cdca src/HOL/Tools/refute.ML
--- 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)
 					)