--- 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)
--- 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}
--- 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))
--- 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]
--- 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 @
--- 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];
--- 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];
--- 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);
--- 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))" *)
--- 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 := []
--- 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
--- 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 =
--- 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;
--- 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
--- 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"
--- 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)
--- 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]
--- 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;
--- 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;
--- 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
--- 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)
--- 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
--- 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)