tuned signature;

--- a/src/Provers/classical.ML	Mon Mar 12 13:53:26 2012 +0100
+++ b/src/Provers/classical.ML	Mon Mar 12 15:31:30 2012 +0100
@@ -301,9 +301,9 @@
     error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
   else Tactic.make_elim th;
 
-fun warn_thm context msg th =
-  if (case context of SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt | _ => false)
-  then warning (msg ^ string_of_thm context th)
+fun warn_thm opt_context msg th =
+  if (case opt_context of SOME context => Context_Position.is_visible_proof context | NONE => false)
+  then warning (msg ^ string_of_thm opt_context th)
   else ();
 
 fun warn_rules context msg rules th =

--- a/src/Pure/context_position.ML	Mon Mar 12 13:53:26 2012 +0100
+++ b/src/Pure/context_position.ML	Mon Mar 12 15:31:30 2012 +0100
@@ -10,6 +10,7 @@
   val set_visible: bool -> Proof.context -> Proof.context
   val restore_visible: Proof.context -> Proof.context -> Proof.context
   val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
+  val is_visible_proof: Context.generic -> bool
   val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit
   val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
   val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
@@ -27,8 +28,10 @@
 
 fun if_visible ctxt f x = if is_visible ctxt then f x else ();
 
-fun if_visible_proof (Context.Proof ctxt) f x = if_visible ctxt f x
-  | if_visible_proof _ _ _ = ();
+fun is_visible_proof (Context.Proof ctxt) = is_visible ctxt
+  | is_visible_proof _ = false;
+
+fun if_visible_proof context f x = if is_visible_proof context then f x else ();
 
 fun reported_text ctxt pos markup txt =
   if is_visible ctxt then Position.reported_text pos markup txt else "";