# HG changeset patch # User wenzelm # Date 1407521833 -7200 # Node ID 56168065136455f40f6cb53f5050be8971545779 # Parent 9665f79a718151f61d502a6c11f7273df1cf1ad9 observe context visibility -- less redundant warnings; diff -r 9665f79a7181 -r 561680651364 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Fri Aug 08 11:43:08 2014 +0200 +++ b/src/HOL/Tools/inductive_set.ML Fri Aug 08 20:17:13 2014 +0200 @@ -275,7 +275,9 @@ Sign.typ_instance thy (U, T')) (Symtab.lookup_list set_arities s') then - (warning ("Ignoring conversion rule for operator " ^ s'); tab) + (if Context_Position.is_really_visible ctxt then + warning ("Ignoring conversion rule for operator " ^ s') + else (); tab) else {to_set_simps = thm :: to_set_simps, to_pred_simps = @@ -289,8 +291,14 @@ | _ => raise Malformed "equation between predicates expected") | _ => raise Malformed "equation expected") handle Malformed msg => - (warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^ - "\n" ^ Display.string_of_thm (Context.proof_of context) thm); tab); + let + val ctxt = Context.proof_of context + val _ = + if Context_Position.is_really_visible ctxt then + warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^ + "\n" ^ Display.string_of_thm ctxt thm) + else (); + in tab end; val pred_set_conv_att = Thm.declaration_attribute (fn thm => fn ctxt => Data.map (add ctxt thm) ctxt);