Eliminated ZCHAFF_VERSION configuration variable, since zChaff's output format is identical in all versions since March 2003 (at least), and also because it forces users who want to use the latest versions to lie about the version number.
I also made the BERKMIN_EXE variable optional, defaulting to BerkMin561 (a reasonable name with no platform encoded in it).
These changes have no inpacts on already working Isabelle installations.

--- a/etc/settings	Wed Feb 18 10:26:48 2009 +0100
+++ b/etc/settings	Tue Feb 24 16:12:27 2009 +0100
@@ -268,8 +268,6 @@
 
 # zChaff (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
 #ZCHAFF_HOME=/usr/local/bin
-#ZCHAFF_VERSION=2004.5.13
-#ZCHAFF_VERSION=2004.11.15
 
 # BerkMin561 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
 #BERKMIN_HOME=/usr/local/bin

--- a/src/HOL/Tools/sat_solver.ML	Wed Feb 18 10:26:48 2009 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Tue Feb 24 16:12:27 2009 +0100
@@ -914,10 +914,6 @@
   fun zchaff fm =
   let
     val _          = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
-    val _          = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso
-                        (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
-      (* both versions of zChaff appear to have the same interface, so we do *)
-      (* not actually need to distinguish between them in the following code *)
     val serial_str = serial_string ()
     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
@@ -943,11 +939,12 @@
 let
   fun berkmin fm =
   let
-    val _          = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
+    val _          = if (getenv "BERKMIN_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
     val serial_str = serial_string ()
     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
-    val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
+    val exec       = getenv "BERKMIN_EXE"
+    val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
     fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
     fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
     val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()