--- a/src/HOL/Library/refute.ML Sun Jan 11 20:45:03 2015 +0100
+++ b/src/HOL/Library/refute.ML Sun Jan 11 21:06:47 2015 +0100
@@ -1025,11 +1025,9 @@
| 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)
@@ -1056,7 +1054,7 @@
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.")
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Sun Jan 11 20:45:03 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Sun Jan 11 21:06:47 2015 +0100
@@ -434,7 +434,7 @@
val (_ : unit list) = ctr_spec_eqn_data_list' |> map (fn (({ctr, ...}, nonexhaustive), x) =>
if length x > 1 then raise PRIMREC ("multiple equations for constructor", map #user_eqn x)
- else if length x = 1 orelse nonexhaustive then ()
+ else if length x = 1 orelse nonexhaustive orelse not (Context_Position.is_visible ctxt) then ()
else warning ("no equation for constructor " ^ Syntax.string_of_term ctxt ctr));
val ctr_spec_eqn_data_list =
--- a/src/HOL/Tools/lin_arith.ML Sun Jan 11 20:45:03 2015 +0100
+++ b/src/HOL/Tools/lin_arith.ML Sun Jan 11 21:06:47 2015 +0100
@@ -301,11 +301,13 @@
"Divides.div_class.mod" (*DYNAMIC BINDING!*),
"Divides.div_class.div" (*DYNAMIC BINDING!*)] a
| _ =>
- (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm);
- false))
+ (if Context_Position.is_visible ctxt then
+ warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
+ else (); false))
| _ =>
- (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm);
- false));
+ (if Context_Position.is_visible ctxt then
+ warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
+ else (); false));
(* substitute new for occurrences of old in a term, incrementing bound *)
(* variables as needed when substituting inside an abstraction *)
@@ -637,12 +639,12 @@
(* code exists above -- in which case either the split theorem should be *)
(* implemented above, or 'is_split_thm' should be modified to filter it *)
(* out *)
- | (t, ts) => (
- warning ("Lin. Arith.: split rule for " ^ Syntax.string_of_term ctxt t ^
- " (with " ^ string_of_int (length ts) ^
- " argument(s)) not implemented; proof reconstruction is likely to fail");
- NONE
- ))
+ | (t, ts) =>
+ (if Context_Position.is_visible ctxt then
+ warning ("Lin. Arith.: split rule for " ^ Syntax.string_of_term ctxt t ^
+ " (with " ^ string_of_int (length ts) ^
+ " argument(s)) not implemented; proof reconstruction is likely to fail")
+ else (); NONE))
end; (* split_once_items *)
(* remove terms that do not satisfy 'p'; change the order of the remaining *)
--- a/src/HOL/Tools/sat.ML Sun Jan 11 20:45:03 2015 +0100
+++ b/src/HOL/Tools/sat.ML Sun Jan 11 21:06:47 2015 +0100
@@ -291,9 +291,10 @@
val clauses'' = filter (fn clause =>
((CNF.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
handle TERM ("dest_Trueprop", _) => false)
- orelse (
- warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
- false)) clauses'
+ orelse
+ (if Context_Position.is_visible ctxt then
+ warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause))
+ else (); false)) clauses'
(* remove trivial clauses -- this is necessary because zChaff removes *)
(* trivial clauses during preprocessing, and otherwise our clause *)
(* numbering would be off *)
@@ -372,7 +373,9 @@
end)
| SAT_Solver.UNSATISFIABLE NONE =>
if Config.get ctxt quick_and_dirty then
- (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
+ (if Context_Position.is_visible ctxt then
+ warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof"
+ else ();
make_quick_and_dirty_thm ())
else
raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])