src/HOL/Library/refute.ML
changeset 56815 848d507584db
parent 56256 1e01c159e7d9
child 56845 691da43fbdd4
     1.1 --- a/src/HOL/Library/refute.ML	Thu May 01 22:41:03 2014 +0200
     1.2 +++ b/src/HOL/Library/refute.ML	Thu May 01 22:56:59 2014 +0200
     1.3 @@ -1068,7 +1068,7 @@
     1.4              val fm_ax = Prop_Logic.all (map toTrue (tl intrs))
     1.5              val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u]
     1.6              val _ =
     1.7 -              (if satsolver = "dpll" orelse satsolver = "enumerate" then
     1.8 +              (if member (op =) ["dpll_p", "dpll", "enumerate"] satsolver then
     1.9                  warning ("Using SAT solver " ^ quote satsolver ^
    1.10                           "; for better performance, consider installing an \
    1.11                           \external solver.")