changeset 57859 | 29e728588163 |
parent 56334 | 6b3739fee456 |
child 58048 | aa6296d09e0e |
--- a/src/Provers/classical.ML Tue Aug 05 11:06:36 2014 +0200 +++ b/src/Provers/classical.ML Tue Aug 05 12:01:32 2014 +0200 @@ -309,7 +309,7 @@ else Tactic.make_elim th; fun warn_thm (SOME (Context.Proof ctxt)) msg th = - if Context_Position.is_visible ctxt + if Context_Position.is_really_visible ctxt then warning (msg ^ Display.string_of_thm ctxt th) else () | warn_thm _ _ _ = ();