src/HOL/Library/refute.ML
changeset 59352 63c02d051661
parent 58893 9e0ecb66d6a7
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/Library/refute.ML	Sun Jan 11 20:45:03 2015 +0100
     1.2 +++ b/src/HOL/Library/refute.ML	Sun Jan 11 21:06:47 2015 +0100
     1.3 @@ -1025,11 +1025,9 @@
     1.4                | NONE => false)
     1.5            | _ => false) types
     1.6          val _ =
     1.7 -          if maybe_spurious then
     1.8 -            warning ("Term contains a recursive datatype; "
     1.9 -              ^ "countermodel(s) may be spurious!")
    1.10 -          else
    1.11 -            ()
    1.12 +          if maybe_spurious andalso Context_Position.is_visible ctxt then
    1.13 +            warning "Term contains a recursive datatype; countermodel(s) may be spurious!"
    1.14 +          else ()
    1.15          fun find_model_loop universe =
    1.16            let
    1.17              val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
    1.18 @@ -1056,7 +1054,7 @@
    1.19              val fm_ax = Prop_Logic.all (map toTrue (tl intrs))
    1.20              val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u]
    1.21              val _ =
    1.22 -              (if member (op =) ["cdclite"] satsolver then
    1.23 +              (if member (op =) ["cdclite"] satsolver andalso Context_Position.is_visible ctxt then
    1.24                  warning ("Using SAT solver " ^ quote satsolver ^
    1.25                           "; for better performance, consider installing an \
    1.26                           \external solver.")