src/Provers/classical.ML
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 _ _ _ = ();