src/HOL/Library/refute.ML

                       Library.exists Old_Datatype_Aux.is_rec_type ds) constrs
                   end
               | NONE => false)
           | _ => false) types
         val _ =
-          if maybe_spurious then
-            warning ("Term contains a recursive datatype; "
-              ^ "countermodel(s) may be spurious!")
-          else
-            ()
+          if maybe_spurious andalso Context_Position.is_visible ctxt then
+            warning "Term contains a recursive datatype; countermodel(s) may be spurious!"
+          else ()
         fun find_model_loop universe =
           let
             val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
             val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime
                     orelse raise TimeLimit.TimeOut

             (* add the well-formedness side condition                       *)
             val fm_u = (if negate then toFalse else toTrue) (hd intrs)
             val fm_ax = Prop_Logic.all (map toTrue (tl intrs))
             val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u]
             val _ =
-              (if member (op =) ["cdclite"] satsolver then
+              (if member (op =) ["cdclite"] satsolver andalso Context_Position.is_visible ctxt then
                 warning ("Using SAT solver " ^ quote satsolver ^
                          "; for better performance, consider installing an \
                          \external solver.")
                else ());
             val solver =