# HG changeset patch
# User wenzelm
# Date 1266592305 -3600
# Node ID f588e1169c8bfaef9a480152ae9456ebdda2a2cd
# Parent  98e52f522357e128f041b7616076739efefbe475
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;

diff -r 98e52f522357 -r f588e1169c8b src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/FOL/simpdata.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -128,7 +128,7 @@
 
 (*No simprules, but basic infastructure for simplification*)
 val FOL_basic_ss =
-  Simplifier.theory_context @{theory} empty_ss
+  Simplifier.global_context @{theory} empty_ss
   setsubgoaler asm_simp_tac
   setSSolver (mk_solver "FOL safe" safe_solver)
   setSolver (mk_solver "FOL unsafe" unsafe_solver)
diff -r 98e52f522357 -r f588e1169c8b src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -82,12 +82,12 @@
     (* Transform the term*)
     val (t,np,nh) = prepare_for_linr thy q g
     (* Some simpsets for dealing with mod div abs and nat*)
-    val simpset0 = Simplifier.theory_context thy HOL_basic_ss addsimps comp_arith
+    val simpset0 = Simplifier.global_context thy HOL_basic_ss addsimps comp_arith
     val ct = cterm_of thy (HOLogic.mk_Trueprop t)
     (* Theorem for the nat --> int transformation *)
    val pre_thm = Seq.hd (EVERY
       [simp_tac simpset0 1,
-       TRY (simp_tac (Simplifier.theory_context thy ferrack_ss) 1)]
+       TRY (simp_tac (Simplifier.global_context thy ferrack_ss) 1)]
       (trivial ct))
     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     (* The result of the quantifier elimination *)
diff -r 98e52f522357 -r f588e1169c8b src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -1248,7 +1248,7 @@
 fun rewrite_hol4_term t thy =
     let
         val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
-        val hol4ss = Simplifier.theory_context thy empty_ss
+        val hol4ss = Simplifier.global_context thy empty_ss
           setmksimps single addsimps hol4rews1
     in
         Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
diff -r 98e52f522357 -r f588e1169c8b src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Import/shuffler.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -488,7 +488,7 @@
 fun norm_term thy t =
     let
         val norms = ShuffleData.get thy
-        val ss = Simplifier.theory_context thy empty_ss
+        val ss = Simplifier.global_context thy empty_ss
           setmksimps single
           addsimps (map (Thm.transfer thy) norms)
           addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
diff -r 98e52f522357 -r f588e1169c8b src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -1547,7 +1547,7 @@
             (augment_sort thy1 pt_cp_sort
               (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
             (fn _ => rtac rec_induct 1 THEN REPEAT
-               (simp_tac (Simplifier.theory_context thy11 HOL_basic_ss
+               (simp_tac (Simplifier.global_context thy11 HOL_basic_ss
                   addsimps flat perm_simps'
                   addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
                 (resolve_tac rec_intrs THEN_ALL_NEW
@@ -1951,7 +1951,7 @@
                           (HOLogic.mk_Trueprop (fresh_const aT rT $ b $ lhs'))
                           (fn _ => EVERY
                              [cut_facts_tac [th'] 1,
-                              full_simp_tac (Simplifier.theory_context thy11 HOL_ss
+                              full_simp_tac (Simplifier.global_context thy11 HOL_ss
                                 addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap
                                 addsimprocs [NominalPermeq.perm_simproc_app]) 1,
                               full_simp_tac (HOL_ss addsimps (calc_atm @
diff -r 98e52f522357 -r f588e1169c8b src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -274,7 +274,7 @@
     val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
     val pt2_atoms = map (fn aT => PureThy.get_thm thy
       ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
-    val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
+    val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
       addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
       addsimprocs [mk_perm_bool_simproc ["Fun.id"],
         NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
@@ -455,7 +455,7 @@
                    concl))
           in map mk_prem prems end) cases_prems;
 
-    val cases_eqvt_ss = Simplifier.theory_context thy HOL_ss
+    val cases_eqvt_ss = Simplifier.global_context thy HOL_ss
       addsimps eqvt_thms @ swap_simps @ perm_pi_simp
       addsimprocs [NominalPermeq.perm_simproc_app,
         NominalPermeq.perm_simproc_fun];
@@ -611,7 +611,7 @@
          atoms)
       end;
     val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
-    val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss addsimps
+    val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps
       (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
       [mk_perm_bool_simproc names,
        NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
diff -r 98e52f522357 -r f588e1169c8b src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -292,7 +292,7 @@
     val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
     val pt2_atoms = map (fn a => PureThy.get_thm thy
       ("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
-    val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
+    val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
       addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
       addsimprocs [mk_perm_bool_simproc ["Fun.id"],
         NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
diff -r 98e52f522357 -r f588e1169c8b src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -143,7 +143,7 @@
 fun perm_simp_gen stac dyn_thms eqvt_thms ss i = 
     ("general simplification of permutations", fn st =>
     let
-       val ss' = Simplifier.theory_context (theory_of_thm st) ss
+       val ss' = Simplifier.global_context (theory_of_thm st) ss
          addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms)
          delcongs weak_congs
          addcongs strong_congs
@@ -221,7 +221,7 @@
   ("analysing permutation compositions on the lhs",
    fn st => EVERY
      [rtac trans i,
-      asm_full_simp_tac (Simplifier.theory_context (theory_of_thm st) empty_ss
+      asm_full_simp_tac (Simplifier.global_context (theory_of_thm st) empty_ss
         addsimprocs [perm_compose_simproc]) i,
       asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i] st);
 
diff -r 98e52f522357 -r f588e1169c8b src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Prolog/prolog.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -59,7 +59,7 @@
 in map zero_var_indexes (at thm) end;
 
 val atomize_ss =
-  Simplifier.theory_context @{theory} empty_ss
+  Simplifier.global_context @{theory} empty_ss
   setmksimps (mksimps mksimps_pairs)
   addsimps [
         all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
diff -r 98e52f522357 -r f588e1169c8b src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Tools/TFL/rules.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -663,7 +663,7 @@
 
 fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
  let val globals = func::G
-     val ss0 = Simplifier.theory_context (Thm.theory_of_thm th) empty_ss
+     val ss0 = Simplifier.global_context (Thm.theory_of_thm th) empty_ss
      val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection];
      val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
      val dummy = term_ref := []
diff -r 98e52f522357 -r f588e1169c8b src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -440,7 +440,7 @@
      (*case_ss causes minimal simplification: bodies of case expressions are
        not simplified. Otherwise large examples (Red-Black trees) are too
        slow.*)
-     val case_ss = Simplifier.theory_context theory
+     val case_ss = Simplifier.global_context theory
        (HOL_basic_ss addcongs
          (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) theory addsimps case_rewrites)
      val corollaries' = map (Simplifier.simplify case_ss) corollaries
diff -r 98e52f522357 -r f588e1169c8b src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -859,7 +859,7 @@
     addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
       @{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}];
   fun prem_nnf_tac i st =
-    full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st;
+    full_simp_tac (Simplifier.global_context (Thm.theory_of_thm st) nnf_simpset) i st;
 in
 fun refute_tac test prep_tac ref_tac =
   let val refute_prems_tac =
diff -r 98e52f522357 -r f588e1169c8b src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Tools/record.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -518,7 +518,7 @@
 
 val is_selector = Symtab.defined o #selectors o get_sel_upd;
 val get_updates = Symtab.lookup o #updates o get_sel_upd;
-fun get_ss_with_context getss thy = Simplifier.theory_context thy (getss (get_sel_upd thy));
+fun get_ss_with_context getss thy = Simplifier.global_context thy (getss (get_sel_upd thy));
 
 val get_simpset = get_ss_with_context #simpset;
 val get_sel_upd_defs = get_ss_with_context #defset;
diff -r 98e52f522357 -r f588e1169c8b src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Tools/simpdata.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -164,7 +164,7 @@
    ("HOL.If", [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
 
 val HOL_basic_ss =
-  Simplifier.theory_context @{theory} empty_ss
+  Simplifier.global_context @{theory} empty_ss
     setsubgoaler asm_simp_tac
     setSSolver safe_solver
     setSolver unsafe_solver
diff -r 98e52f522357 -r f588e1169c8b src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/Provers/hypsubst.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -156,7 +156,7 @@
     let fun tac i st = SUBGOAL (fn (Bi, _) =>
       let
         val (k, _) = eq_var bnd true Bi
-        val hyp_subst_ss = Simplifier.theory_context (Thm.theory_of_thm st) empty_ss
+        val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
           setmksimps (mk_eqs bnd)
       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
         etac thin_rl i, rotate_tac (~k) i]
diff -r 98e52f522357 -r f588e1169c8b src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/Pure/codegen.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -299,7 +299,7 @@
 val del_unfold = map_unfold o MetaSimplifier.del_simp;
 
 fun unfold_preprocessor thy =
-  let val ss = Simplifier.theory_context thy (UnfoldData.get thy)
+  let val ss = Simplifier.global_context thy (UnfoldData.get thy)
   in map (Thm.transfer thy #> Simplifier.full_simplify ss) end;
 
 
diff -r 98e52f522357 -r f588e1169c8b src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/Pure/meta_simplifier.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -111,7 +111,7 @@
   val inherit_context: simpset -> simpset -> simpset
   val the_context: simpset -> Proof.context
   val context: Proof.context -> simpset -> simpset
-  val theory_context: theory  -> simpset -> simpset
+  val global_context: theory  -> 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
@@ -341,7 +341,7 @@
 fun context ctxt =
   map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt));
 
-val theory_context = context o ProofContext.init;
+val global_context = context o ProofContext.init;
 
 fun activate_context thy ss =
   let
@@ -1241,7 +1241,7 @@
 
 fun rewrite _ [] ct = Thm.reflexive ct
   | rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover
-      (theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
+      (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
 
 fun simplify full thms = Conv.fconv_rule (rewrite full thms);
 val rewrite_rule = simplify true;
@@ -1255,7 +1255,7 @@
 (*Rewrite the subgoals of a proof state (represented by a theorem)*)
 fun rewrite_goals_rule thms th =
   Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
-    (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
+    (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
 
 (*Rewrite the subgoal of a proof state (represented by a theorem)*)
 fun rewrite_goal_rule mode prover ss i thm =
@@ -1279,7 +1279,7 @@
 fun rewrite_goal_tac rews =
   let val ss = empty_ss addsimps rews in
     fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
-      (theory_context (Thm.theory_of_thm st) ss) i st
+      (global_context (Thm.theory_of_thm st) ss) i st
   end;
 
 (*Prunes all redundant parameters from the proof state by rewriting.
@@ -1317,7 +1317,7 @@
 fun gen_norm_hhf ss th =
   (if Drule.is_norm_hhf (Thm.prop_of th) then th
    else Conv.fconv_rule
-    (rewrite_cterm (true, false, false) (K (K NONE)) (theory_context (Thm.theory_of_thm th) ss)) th)
+    (rewrite_cterm (true, false, false) (K (K NONE)) (global_context (Thm.theory_of_thm th) ss)) th)
   |> Thm.adjust_maxidx_thm ~1
   |> Drule.gen_all;
 
diff -r 98e52f522357 -r f588e1169c8b src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/Pure/simplifier.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -36,7 +36,7 @@
   val inherit_context: simpset -> simpset -> simpset
   val the_context: simpset -> Proof.context
   val context: Proof.context -> simpset -> simpset
-  val theory_context: theory  -> simpset -> simpset
+  val global_context: theory  -> simpset -> simpset
   val simproc_i: theory -> string -> term list
     -> (theory -> simpset -> term -> thm option) -> simproc
   val simproc: theory -> string -> string list
diff -r 98e52f522357 -r f588e1169c8b src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/Sequents/simpdata.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -68,7 +68,7 @@
 
 (*No simprules, but basic infrastructure for simplification*)
 val LK_basic_ss =
-  Simplifier.theory_context @{theory} empty_ss
+  Simplifier.global_context @{theory} empty_ss
     setsubgoaler asm_simp_tac
     setSSolver (mk_solver "safe" safe_solver)
     setSolver (mk_solver "unsafe" unsafe_solver)
diff -r 98e52f522357 -r f588e1169c8b src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -129,7 +129,7 @@
 
 fun preprocess thy =
   let
-    val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
+    val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
   in
     preprocess_functrans thy
     #> (map o apfst) (rewrite_eqn pre)
@@ -137,7 +137,7 @@
 
 fun preprocess_conv thy ct =
   let
-    val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
+    val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
   in
     ct
     |> Simplifier.rewrite pre
@@ -146,7 +146,7 @@
 
 fun postprocess_conv thy ct =
   let
-    val post = (Simplifier.theory_context thy o #post o the_thmproc) thy;
+    val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
   in
     ct
     |> AxClass.overload_conv thy
diff -r 98e52f522357 -r f588e1169c8b src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -327,7 +327,7 @@
 
      (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
        If the premises get simplified, then the proofs could fail.*)
-     val min_ss = Simplifier.theory_context thy empty_ss
+     val min_ss = Simplifier.global_context thy empty_ss
            setmksimps (map mk_eq o ZF_atomize o gen_all)
            setSolver (mk_solver "minimal"
                       (fn prems => resolve_tac (triv_rls@prems)