src/HOL/Library/refute.ML
changeset 56851 35ff4ede3409
parent 56846 9df717fef2bb
child 56853 a265e41cc33b
     1.1 --- a/src/HOL/Library/refute.ML	Sun May 04 18:53:58 2014 +0200
     1.2 +++ b/src/HOL/Library/refute.ML	Sun May 04 18:57:45 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 member (op =) ["dpll_p"] satsolver then
     1.8 +              (if member (op =) ["cdclite"] satsolver then
     1.9                  warning ("Using SAT solver " ^ quote satsolver ^
    1.10                           "; for better performance, consider installing an \
    1.11                           \external solver.")