diff -r eb8f2a5a57ad -r 848d507584db src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu May 01 22:41:03 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu May 01 22:56:59 2014 +0200
@@ -574,7 +574,7 @@
         (* use the first ML solver (to avoid startup overhead) *)
         val (ml_solvers, nonml_solvers) =
           SatSolver.get_solvers ()
-          |> List.partition (member (op =) ["dptsat", "dpll"] o fst)
+          |> List.partition (member (op =) ["dptsat", "dpll_p", "dpll"] o fst)
         val res =
           if null nonml_solvers then
             TimeLimit.timeLimit tac_timeout (snd (hd ml_solvers)) prop