# HG changeset patch
# User wenzelm
# Date 1407232892 -7200
# Node ID 29e728588163b5fa467cf99f33ce49223821021b
# Parent  39d9c7f175e06f011403a62c89212649ed1ff90f
more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073) -- avoid duplicate warnings;

diff -r 39d9c7f175e0 -r 29e728588163 src/Provers/classical.ML
--- 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 _ _ _ = ();
 
diff -r 39d9c7f175e0 -r 29e728588163 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Aug 05 11:06:36 2014 +0200
+++ b/src/Pure/raw_simplifier.ML	Tue Aug 05 12:01:32 2014 +0200
@@ -385,7 +385,7 @@
     val thy' = Proof_Context.theory_of ctxt';
   in Context.theory_map (Simpset.map (K (simpset_of ctxt'))) thy' end;
 
-fun map_ss f = Context.mapping (map_theory_simpset f) f;
+fun map_ss f = Context.mapping (map_theory_simpset (f o Context_Position.not_really)) f;
 
 val clear_simpset =
   map_simpset (fn Simpset ({depth, ...}, {mk_rews, termless, subgoal_tac, solvers, ...}) =>
@@ -428,7 +428,7 @@
 val simp_trace = Config.bool simp_trace_raw;
 
 fun cond_warning ctxt msg =
-  if Context_Position.is_visible ctxt then warning (msg ()) else ();
+  if Context_Position.is_really_visible ctxt then warning (msg ()) else ();
 
 fun cond_tracing' ctxt flag msg =
   if Config.get ctxt flag then
@@ -593,6 +593,7 @@
 fun add_simp thm ctxt = ctxt addsimps [thm];
 fun del_simp thm ctxt = ctxt delsimps [thm];
 
+
 (* congs *)
 
 local
diff -r 39d9c7f175e0 -r 29e728588163 src/Sequents/prover.ML
--- 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))));