--- a/src/Sequents/prover.ML Tue Aug 05 11:06:36 2014 +0200
+++ b/src/Sequents/prover.ML Tue Aug 05 12:01:32 2014 +0200
@@ -78,11 +78,13 @@
Pack (rules |> which (fn ths =>
if member Thm.eq_thm_prop ths th then
let
- val ctxt = Context.proof_of context;
val _ =
- if Context_Position.is_visible ctxt then
- warning ("Ignoring duplicate theorems:\n" ^ Display.string_of_thm ctxt th)
- else ();
+ (case context of
+ Context.Proof ctxt =>
+ if Context_Position.is_really_visible ctxt then
+ warning ("Ignoring duplicate theorems:\n" ^ Display.string_of_thm ctxt th)
+ else ()
+ | _ => ());
in ths end
else sort_rules (th :: ths))));