--- 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