# HG changeset patch
# User wenzelm
# Date 1272643961 -7200
# Node ID 04dd306fdb3cc748eac8dac47ad16ec222480bb2
# Parent  663bb2bc1e72de930e15131eeb414f7bf8603a83# Parent  a9873318fe30785576a82505ceb73f3717b5cfdb
merged

diff -r 663bb2bc1e72 -r 04dd306fdb3c src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Apr 30 17:53:49 2010 +0200
+++ b/src/FOL/simpdata.ML	Fri Apr 30 18:12:41 2010 +0200
@@ -21,13 +21,13 @@
   | _                           => th RS @{thm iff_reflection_T};
 
 (*Replace premises x=y, X<->Y by X==Y*)
-val mk_meta_prems =
-    rule_by_tactic
+fun mk_meta_prems ctxt =
+    rule_by_tactic ctxt
       (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
 
 (*Congruence rules for = or <-> (instead of ==)*)
-fun mk_meta_cong (_: simpset) rl =
-  Drule.export_without_context (mk_meta_eq (mk_meta_prems rl))
+fun mk_meta_cong ss rl =
+  Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
     handle THM _ =>
       error("Premises and conclusion of congruence rules must use =-equality or <->");
 
diff -r 663bb2bc1e72 -r 04dd306fdb3c src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Fri Apr 30 17:53:49 2010 +0200
+++ b/src/HOL/Tools/TFL/post.ML	Fri Apr 30 18:12:41 2010 +0200
@@ -128,9 +128,9 @@
   Split_Rule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl;
 
 (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
-val meta_outer =
+fun meta_outer ctxt =
   curry_rule o Drule.export_without_context o
-  rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
+  rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
 
 (*Strip off the outer !P*)
 val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
@@ -139,7 +139,9 @@
   | tracing false msg = writeln msg;
 
 fun simplify_defn strict thy cs ss congs wfs id pats def0 =
-   let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
+   let
+       val ctxt = ProofContext.init thy
+       val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
        val {rules,rows,TCs,full_pats_TCs} =
            Prim.post_definition congs (thy, (def,pats))
        val {lhs=f,rhs} = S.dest_eq (concl def)
@@ -153,7 +155,7 @@
                 TCs = TCs}
        val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
                         (R.CONJUNCTS rules)
-         in  {induct = meta_outer (Object_Logic.rulify_no_asm (induction RS spec')),
+         in  {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')),
         rules = ListPair.zip(rules', rows),
         tcs = (termination_goals rules') @ tcs}
    end
diff -r 663bb2bc1e72 -r 04dd306fdb3c src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Apr 30 17:53:49 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Fri Apr 30 18:12:41 2010 +0200
@@ -446,7 +446,7 @@
     val cprop = Thm.cterm_of thy prop;
     val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac;
     fun mk_elim rl =
-      Thm.implies_intr cprop (Tactic.rule_by_tactic tac (Thm.assume cprop RS rl))
+      Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
       |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
   in
     (case get_first (try mk_elim) elims of
diff -r 663bb2bc1e72 -r 04dd306fdb3c src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Fri Apr 30 17:53:49 2010 +0200
+++ b/src/HOL/Tools/split_rule.ML	Fri Apr 30 18:12:41 2010 +0200
@@ -116,7 +116,7 @@
 
 fun split_rule_goal ctxt xss rl =
   let
-    fun one_split i s = Tactic.rule_by_tactic (pair_tac ctxt s i);
+    fun one_split i s = Tactic.rule_by_tactic ctxt (pair_tac ctxt s i);
     fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
   in
     rl
diff -r 663bb2bc1e72 -r 04dd306fdb3c src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Apr 30 17:53:49 2010 +0200
+++ b/src/Provers/classical.ML	Fri Apr 30 18:12:41 2010 +0200
@@ -208,8 +208,11 @@
 fun dup_intr th = zero_var_indexes (th RS classical);
 
 fun dup_elim th =
-    rule_by_tactic (TRYALL (etac revcut_rl))
-      ((th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd);
+  let
+    val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
+    val ctxt = ProofContext.init (Thm.theory_of_thm rl);
+  in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
+
 
 (**** Classical rule sets ****)
 
diff -r 663bb2bc1e72 -r 04dd306fdb3c src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Fri Apr 30 17:53:49 2010 +0200
+++ b/src/Pure/meta_simplifier.ML	Fri Apr 30 18:12:41 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 663bb2bc1e72 -r 04dd306fdb3c src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Apr 30 17:53:49 2010 +0200
+++ b/src/Pure/simplifier.ML	Fri Apr 30 18:12:41 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 *)
diff -r 663bb2bc1e72 -r 04dd306fdb3c src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Apr 30 17:53:49 2010 +0200
+++ b/src/Pure/tactic.ML	Fri Apr 30 18:12:41 2010 +0200
@@ -7,7 +7,7 @@
 signature BASIC_TACTIC =
 sig
   val trace_goalno_tac: (int -> tactic) -> int -> tactic
-  val rule_by_tactic: tactic -> thm -> thm
+  val rule_by_tactic: Proof.context -> tactic -> thm -> thm
   val assume_tac: int -> tactic
   val eq_assume_tac: int -> tactic
   val compose_tac: (bool * thm * int) -> int -> tactic
@@ -86,14 +86,14 @@
                          Seq.make(fn()=> seqcell));
 
 (*Makes a rule by applying a tactic to an existing rule*)
-fun rule_by_tactic tac rl =
+fun rule_by_tactic ctxt tac rl =
   let
-    val ctxt = Variable.thm_context rl;
-    val ((_, [st]), ctxt') = Variable.import true [rl] ctxt;
+    val ctxt' = Variable.declare_thm rl ctxt;
+    val ((_, [st]), ctxt'') = Variable.import true [rl] ctxt';
   in
     (case Seq.pull (tac st) of
       NONE => raise THM ("rule_by_tactic", 0, [rl])
-    | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st'))
+    | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt'' ctxt') st'))
   end;
 
 
diff -r 663bb2bc1e72 -r 04dd306fdb3c src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Fri Apr 30 17:53:49 2010 +0200
+++ b/src/Sequents/simpdata.ML	Fri Apr 30 18:12:41 2010 +0200
@@ -42,13 +42,13 @@
                          Display.string_of_thm_without_context th));
 
 (*Replace premises x=y, X<->Y by X==Y*)
-val mk_meta_prems =
-    rule_by_tactic
+fun mk_meta_prems ctxt =
+    rule_by_tactic ctxt
       (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
 
 (*Congruence rules for = or <-> (instead of ==)*)
-fun mk_meta_cong (_: simpset) rl =
-  Drule.export_without_context(mk_meta_eq (mk_meta_prems rl))
+fun mk_meta_cong ss rl =
+  Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
     handle THM _ =>
       error("Premises and conclusion of congruence rules must use =-equality or <->");
 
diff -r 663bb2bc1e72 -r 04dd306fdb3c src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri Apr 30 17:53:49 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Fri Apr 30 18:12:41 2010 +0200
@@ -261,7 +261,7 @@
       THEN (PRIMITIVE (fold_rule part_rec_defs));
 
   (*Elimination*)
-  val elim = rule_by_tactic basic_elim_tac
+  val elim = rule_by_tactic (ProofContext.init thy1) basic_elim_tac
                  (unfold RS Ind_Syntax.equals_CollectD)
 
   (*Applies freeness of the given constructors, which *must* be unfolded by
@@ -269,7 +269,7 @@
       con_defs=[] for inference systems.
     Proposition A should have the form t:Si where Si is an inductive set*)
   fun make_cases ctxt A =
-    rule_by_tactic
+    rule_by_tactic ctxt
       (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac (simpset_of ctxt)) THEN basic_elim_tac)
       (Thm.assume A RS elim)
       |> Drule.export_without_context_open;