1.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Aug 08 11:43:08 2014 +0200
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Aug 08 20:17:13 2014 +0200
     1.3 @@ -275,7 +275,9 @@
     1.4                     Sign.typ_instance thy (U, T'))
     1.5                       (Symtab.lookup_list set_arities s')
     1.6                   then
     1.7 -                   (warning ("Ignoring conversion rule for operator " ^ s'); tab)
     1.8 +                   (if Context_Position.is_really_visible ctxt then
     1.9 +                     warning ("Ignoring conversion rule for operator " ^ s')
    1.10 +                    else (); tab)
    1.11                   else
    1.12                     {to_set_simps = thm :: to_set_simps,
    1.13                      to_pred_simps =
    1.14 @@ -289,8 +291,14 @@
    1.15         | _ => raise Malformed "equation between predicates expected")
    1.16    | _ => raise Malformed "equation expected")
    1.17    handle Malformed msg =>
    1.18 -    (warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^
    1.19 -      "\n" ^ Display.string_of_thm (Context.proof_of context) thm); tab);
    1.20 +    let
    1.21 +      val ctxt = Context.proof_of context
    1.22 +      val _ =
    1.23 +        if Context_Position.is_really_visible ctxt then
    1.24 +          warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^
    1.25 +            "\n" ^ Display.string_of_thm ctxt thm)
    1.26 +        else ();
    1.27 +    in tab end;
    1.28  
    1.29  val pred_set_conv_att = Thm.declaration_attribute
    1.30    (fn thm => fn ctxt => Data.map (add ctxt thm) ctxt);