make 'dpll_p' the default SAT solver, rather than the hard-to-get zChaff-with-proofs

--- a/src/HOL/Tools/sat.ML	Sun May 04 18:14:59 2014 +0200
+++ b/src/HOL/Tools/sat.ML	Sun May 04 18:50:42 2014 +0200
@@ -65,7 +65,7 @@
 fun cond_tracing ctxt msg =
   if Config.get ctxt trace then tracing (msg ()) else ();
 
-val solver = Attrib.setup_config_string @{binding sat_solver} (K "zchaff_with_proofs");
+val solver = Attrib.setup_config_string @{binding sat_solver} (K "dpll_p");
   (*see HOL/Tools/sat_solver.ML for possible values*)
 
 val counter = Unsynchronized.ref 0;