# 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);