# HG changeset patch
# User wenzelm
# Date 1272640709 -7200
# Node ID 5c5b5c7f11572ff4c321c2446b1fd023a50c6f09
# Parent  8da6846b87d9b49ed24f96fac0d9e3389ad504f2
conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context;
map_ss: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;

diff -r 8da6846b87d9 -r 5c5b5c7f1157 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu Apr 29 23:55:43 2010 +0200
+++ b/src/Pure/meta_simplifier.ML	Fri Apr 30 17:18:29 2010 +0200
@@ -115,6 +115,7 @@
   val the_context: simpset -> Proof.context
   val context: Proof.context -> simpset -> simpset
   val global_context: theory  -> simpset -> simpset
+  val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
   val debug_bounds: bool Unsynchronized.ref
   val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
   val set_solvers: solver list -> simpset -> simpset
@@ -326,7 +327,8 @@
   print_term_global ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th);
 
 fun cond_warn_thm a (ss as Simpset ({context, ...}, _)) th =
-  if is_some context then () else warn_thm a ss th;
+  if (case context of NONE => true | SOME ctxt => Context_Position.is_visible ctxt)
+  then warn_thm a ss th else ();
 
 end;
 
@@ -358,9 +360,13 @@
 fun activate_context thy ss =
   let
     val ctxt = the_context ss;
-    val ctxt' = Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt)) ctxt;
+    val ctxt' = ctxt
+      |> Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt))
+      |> Context_Position.set_visible false;
   in context ctxt' ss end;
 
+fun with_context ctxt f ss = inherit_context ss (f (context ctxt ss));
+
 
 (* maintain simp rules *)
 
diff -r 8da6846b87d9 -r 5c5b5c7f1157 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Apr 29 23:55:43 2010 +0200
+++ b/src/Pure/simplifier.ML	Fri Apr 30 17:18:29 2010 +0200
@@ -108,7 +108,7 @@
 );
 
 val get_ss = SimpsetData.get;
-val map_ss = SimpsetData.map;
+fun map_ss f context = SimpsetData.map (with_context (Context.proof_of context) f) context;
 
 
 (* attributes *)