src/Provers/classical.ML
changeset 52699 abed4121c17e
parent 52462 a241826ed003
child 52732 b4da1f2ec73f
     1.1 --- a/src/Provers/classical.ML	Thu Jul 18 21:06:21 2013 +0200
     1.2 +++ b/src/Provers/classical.ML	Thu Jul 18 21:20:09 2013 +0200
     1.3 @@ -302,10 +302,10 @@
     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 opt_context msg th =
     1.8 -  if (case opt_context of SOME context => Context_Position.is_visible_proof context | NONE => false)
     1.9 -  then warning (msg ^ string_of_thm opt_context th)
    1.10 -  else ();
    1.11 +fun warn_thm (SOME (Context.Proof ctxt)) msg th =
    1.12 +      if Context_Position.is_visible ctxt
    1.13 +      then warning (msg ^ Display.string_of_thm ctxt th) else ()
    1.14 +  | warn_thm _ _ _ = ();
    1.15  
    1.16  fun warn_rules context msg rules th =
    1.17    Item_Net.member rules th andalso (warn_thm context msg th; true);