# HG changeset patch # User wenzelm # Date 1266595433 -3600 # Node ID 7c7cfe69d7f6c8f7ba887de45e3d70d4b6042fd4 # Parent d4ec25836a787ae332845e344b945fb792b557bc# Parent 7508302738ea28f2ddc91fdfc60226129143070f merged diff -r d4ec25836a78 -r 7c7cfe69d7f6 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/FOL/simpdata.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Fri Feb 19 17:03:53 2010 +0100 @@ -72,26 +72,25 @@ fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp; -fun linr_tac ctxt q i = - (ObjectLogic.atomize_prems_tac i) - THEN (REPEAT_DETERM (split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}] i)) - THEN (fn st => +fun linr_tac ctxt q = + ObjectLogic.atomize_prems_tac + THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}]) + THEN' SUBGOAL (fn (g, i) => let - val g = List.nth (prems_of st, i - 1) val thy = ProofContext.theory_of ctxt (* 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.context ctxt 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.context ctxt ferrack_ss) 1)] (trivial ct)) fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) (* The result of the quantifier elimination *) - val (th, tac) = case (prop_of pre_thm) of + val (th, tac) = case prop_of pre_thm of Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ => let val pth = linr_oracle (cterm_of thy (Pattern.eta_long [] t1)) in @@ -101,9 +100,7 @@ assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) end | _ => (pre_thm, assm_tac i) - in (rtac (((mp_step nh) o (spec_step np)) th) i - THEN tac) st - end handle Subscript => no_tac st); + in rtac ((mp_step nh o spec_step np) th) i THEN tac end); val setup = Method.setup @{binding rferrack} diff -r d4ec25836a78 -r 7c7cfe69d7f6 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/HOL/Import/proof_kernel.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/HOL/Import/shuffler.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/HOL/Nominal/nominal_permeq.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/HOL/Prolog/prolog.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/HOL/Tools/TFL/rules.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/HOL/Tools/TFL/tfl.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/HOL/Tools/lin_arith.ML Fri Feb 19 17:03:53 2010 +0100 @@ -6,7 +6,7 @@ signature LIN_ARITH = sig - val pre_tac: Proof.context -> int -> tactic + val pre_tac: simpset -> int -> tactic val simple_tac: Proof.context -> int -> tactic val tac: Proof.context -> int -> tactic val simproc: simpset -> term -> thm option @@ -705,13 +705,12 @@ setmksimps (mksimps mksimps_pairs) addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj, not_all, not_ex, not_not] - fun prem_nnf_tac i st = - full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) - i st + fun prem_nnf_tac ss = full_simp_tac (Simplifier.inherit_context ss nnf_simpset) in -fun split_once_tac ctxt split_thms = +fun split_once_tac ss split_thms = let + val ctxt = Simplifier.the_context ss val thy = ProofContext.theory_of ctxt val cond_split_tac = SUBGOAL (fn (subgoal, i) => let @@ -734,7 +733,7 @@ REPEAT_DETERM o etac rev_mp, cond_split_tac, rtac ccontr, - prem_nnf_tac, + prem_nnf_tac ss, TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE)) ] end; @@ -746,15 +745,16 @@ (* subgoals and finally attempt to solve them by finding an immediate *) (* contradiction (i.e., a term and its negation) in their premises. *) -fun pre_tac ctxt i = +fun pre_tac ss i = let + val ctxt = Simplifier.the_context ss; val split_thms = filter is_split_thm (#splits (get_arith_data ctxt)) fun is_relevant t = is_some (decomp ctxt t) in DETERM ( TRY (filter_prems_tac is_relevant i) THEN ( - (TRY o REPEAT_ALL_NEW (split_once_tac ctxt split_thms)) + (TRY o REPEAT_ALL_NEW (split_once_tac ss split_thms)) THEN_ALL_NEW (CONVERSION Drule.beta_eta_conversion THEN' @@ -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 d4ec25836a78 -r 7c7cfe69d7f6 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/HOL/Tools/record.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/HOL/Tools/simpdata.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/HOL/ex/Arith_Examples.thy --- a/src/HOL/ex/Arith_Examples.thy Fri Feb 19 16:42:37 2010 +0100 +++ b/src/HOL/ex/Arith_Examples.thy Fri Feb 19 17:03:53 2010 +0100 @@ -123,12 +123,12 @@ (* FIXME: need to replace 1 by its numeral representation *) apply (subst numeral_1_eq_1 [symmetric]) (* FIXME: arith does not know about iszero *) - apply (tactic {* Lin_Arith.pre_tac @{context} 1 *}) + apply (tactic {* Lin_Arith.pre_tac @{simpset} 1 *}) oops lemma "(i::int) mod 42 <= 41" (* FIXME: arith does not know about iszero *) - apply (tactic {* Lin_Arith.pre_tac @{context} 1 *}) + apply (tactic {* Lin_Arith.pre_tac @{simpset} 1 *}) oops lemma "-(i::int) * 1 = 0 ==> i = 0" diff -r d4ec25836a78 -r 7c7cfe69d7f6 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/Provers/Arith/fast_lin_arith.ML Fri Feb 19 17:03:53 2010 +0100 @@ -56,7 +56,7 @@ val pre_decomp: Proof.context -> typ list * term list -> (typ list * term list) list (*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*) - val pre_tac: Proof.context -> int -> tactic + val pre_tac: simpset -> int -> tactic (*the limit on the number of ~= allowed; because each ~= is split into two cases, this can lead to an explosion*) @@ -792,7 +792,7 @@ (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *) DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN (* user-defined preprocessing of the subgoal *) - DETERM (LA_Data.pre_tac ctxt i) THEN + DETERM (LA_Data.pre_tac ss i) THEN PRIMITIVE (trace_thm ctxt "State after pre_tac:") THEN (* prove every resulting subgoal, using its justification *) EVERY (map just1 justs) diff -r d4ec25836a78 -r 7c7cfe69d7f6 src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/Provers/hypsubst.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/Pure/codegen.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/Pure/meta_simplifier.ML Fri Feb 19 17:03:53 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 @@ -1025,7 +1025,8 @@ val b' = #1 (Term.dest_Free (Thm.term_of v)); val _ = if b <> b' then - warning ("Simplifier: renamed bound variable " ^ quote b ^ " to " ^ quote b') + warning ("Simplifier: renamed bound variable " ^ + quote b ^ " to " ^ quote b' ^ Position.str_of (Position.thread_data ())) else (); val ss' = add_bound ((b', T), a) ss; val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0; @@ -1240,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; @@ -1254,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 = @@ -1278,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. @@ -1316,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 d4ec25836a78 -r 7c7cfe69d7f6 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/Pure/simplifier.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/Sequents/simpdata.ML --- a/src/Sequents/simpdata.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/Sequents/simpdata.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/Tools/Code/code_preproc.ML Fri Feb 19 17:03:53 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 d4ec25836a78 -r 7c7cfe69d7f6 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Fri Feb 19 16:42:37 2010 +0100 +++ b/src/ZF/Tools/inductive_package.ML Fri Feb 19 17:03:53 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)