src/Provers/classical.ML
changeset 46874 993c413746f4
parent 46459 73823dbbecc4
child 46961 5c6955f487e5
     1.1 --- a/src/Provers/classical.ML	Mon Mar 12 13:53:26 2012 +0100
     1.2 +++ b/src/Provers/classical.ML	Mon Mar 12 15:31:30 2012 +0100
     1.3 @@ -301,9 +301,9 @@
     1.4      error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
     1.5    else Tactic.make_elim th;
     1.6  
     1.7 -fun warn_thm context msg th =
     1.8 -  if (case context of SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt | _ => false)
     1.9 -  then warning (msg ^ string_of_thm context th)
    1.10 +fun warn_thm opt_context msg th =
    1.11 +  if (case opt_context of SOME context => Context_Position.is_visible_proof context | NONE => false)
    1.12 +  then warning (msg ^ string_of_thm opt_context th)
    1.13    else ();
    1.14  
    1.15  fun warn_rules context msg rules th =