--- a/TFL/rules.ML Tue Oct 18 17:59:24 2005 +0200
+++ b/TFL/rules.ML Tue Oct 18 17:59:25 2005 +0200
@@ -664,7 +664,8 @@
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
let val globals = func::G
- val pbeta_reduce = simpl_conv empty_ss [split_conv RS eq_reflection];
+ val ss0 = Simplifier.theory_context (Thm.theory_of_thm th) empty_ss
+ val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection];
val tc_list = ref[]: term list ref
val dummy = term_ref := []
val dummy = thm_ref := []
@@ -805,7 +806,7 @@
val ctm = cprop_of th
val names = add_term_names (term_of ctm, [])
val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
- (prover names) (empty_ss addsimps [cut_lemma'] addeqcongs congs) ctm
+ (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
val th2 = equal_elim th1 th
in
(th2, List.filter (not o restricted) (!tc_list))
--- a/src/FOL/simpdata.ML Tue Oct 18 17:59:24 2005 +0200
+++ b/src/FOL/simpdata.ML Tue Oct 18 17:59:25 2005 +0200
@@ -330,7 +330,8 @@
eq_assume_tac, ematch_tac [FalseE]];
(*No simprules, but basic infastructure for simplification*)
-val FOL_basic_ss = empty_ss
+val FOL_basic_ss =
+ Simplifier.theory_context (the_context ()) empty_ss
setsubgoaler asm_simp_tac
setSSolver (mk_solver "FOL safe" safe_solver)
setSolver (mk_solver "FOL unsafe" unsafe_solver)
--- a/src/HOL/Import/shuffler.ML Tue Oct 18 17:59:24 2005 +0200
+++ b/src/HOL/Import/shuffler.ML Tue Oct 18 17:59:25 2005 +0200
@@ -490,8 +490,9 @@
val sg = sign_of thy
val norms = ShuffleData.get thy
- val ss = empty_ss setmksimps single
- addsimps (map (Thm.transfer sg) norms)
+ val ss = Simplifier.theory_context thy empty_ss
+ setmksimps single
+ addsimps (map (Thm.transfer sg) norms)
fun chain f th =
let
val rhs = snd (dest_equals (cprop_of th))
--- a/src/HOL/Prolog/HOHH.ML Tue Oct 18 17:59:24 2005 +0200
+++ b/src/HOL/Prolog/HOHH.ML Tue Oct 18 17:59:25 2005 +0200
@@ -54,7 +54,10 @@
| _ => [thm]
in map zero_var_indexes (at thm) end;
-val atomize_ss = empty_ss setmksimps (mksimps mksimps_pairs) addsimps [
+val atomize_ss =
+ Simplifier.theory_context (the_context ()) empty_ss
+ setmksimps (mksimps mksimps_pairs)
+ addsimps [
all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
imp_conjR, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
--- a/src/HOL/Tools/record_package.ML Tue Oct 18 17:59:24 2005 +0200
+++ b/src/HOL/Tools/record_package.ML Tue Oct 18 17:59:25 2005 +0200
@@ -317,7 +317,7 @@
val is_selector = Symtab.defined o #selectors o get_sel_upd;
val get_updates = Symtab.lookup o #updates o get_sel_upd;
-val get_simpset = #simpset o get_sel_upd;
+fun get_simpset thy = Simplifier.theory_context thy (#simpset (get_sel_upd thy));
fun put_sel_upd names simps thy =
let
@@ -1119,8 +1119,6 @@
fun record_split_simp_tac thms P i st =
let
val sg = Thm.sign_of_thm st;
- val {sel_upd={simpset,...},...}
- = RecordsData.get sg;
val has_rec = exists_Const
(fn (s, Type (_, [Type (_, [T, _]), _])) =>
@@ -1158,7 +1156,7 @@
val simprocs = if has_rec goal then [record_split_simproc P] else [];
in st |> ((EVERY split_frees_tacs)
- THEN (Simplifier.full_simp_tac (simpset addsimps thms addsimprocs simprocs) i))
+ THEN (Simplifier.full_simp_tac (get_simpset sg addsimps thms addsimprocs simprocs) i))
end handle Empty => Seq.empty;
end;
--- a/src/HOL/simpdata.ML Tue Oct 18 17:59:24 2005 +0200
+++ b/src/HOL/simpdata.ML Tue Oct 18 17:59:25 2005 +0200
@@ -341,7 +341,8 @@
val safe_solver = mk_solver "HOL safe" safe_solver_tac;
val HOL_basic_ss =
- empty_ss setsubgoaler asm_simp_tac
+ Simplifier.theory_context (the_context ()) empty_ss
+ setsubgoaler asm_simp_tac
setSSolver safe_solver
setSolver unsafe_solver
setmksimps (mksimps mksimps_pairs)
@@ -460,14 +461,13 @@
*)
local
- val nnf_simps =
- [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj,
- not_all,not_ex,not_not];
val nnf_simpset =
- empty_ss setmkeqTrue mk_eq_True
- setmksimps (mksimps mksimps_pairs)
- addsimps nnf_simps;
- val prem_nnf_tac = full_simp_tac nnf_simpset
+ empty_ss setmkeqTrue mk_eq_True
+ 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;
in
fun refute_tac test prep_tac ref_tac =
let val refute_prems_tac =
--- a/src/Provers/Arith/fast_lin_arith.ML Tue Oct 18 17:59:24 2005 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Tue Oct 18 17:59:25 2005 +0200
@@ -79,7 +79,7 @@
val trace : bool ref
val fast_arith_neq_limit: int ref
val lin_arith_prover: theory -> simpset -> term -> thm option
- val lin_arith_tac: bool -> int -> tactic
+ val lin_arith_tac: bool -> int -> tactic
val cut_lin_arith_tac: simpset -> int -> tactic
end;
@@ -665,7 +665,9 @@
| SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i,js))
end) i st;
-val lin_arith_tac = simpset_lin_arith_tac Simplifier.empty_ss;
+fun lin_arith_tac ex i st =
+ simpset_lin_arith_tac (Simplifier.theory_context (Thm.theory_of_thm st) Simplifier.empty_ss)
+ ex i st;
fun cut_lin_arith_tac ss i =
cut_facts_tac (Simplifier.prems_of_ss ss) i THEN
--- a/src/Pure/tactic.ML Tue Oct 18 17:59:24 2005 +0200
+++ b/src/Pure/tactic.ML Tue Oct 18 17:59:25 2005 +0200
@@ -535,8 +535,10 @@
val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
fun rewrite_goal_tac rews =
- MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac)
- (MetaSimplifier.empty_ss addsimps rews);
+ let val ss = MetaSimplifier.empty_ss addsimps rews in
+ fn i => fn st => MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac)
+ (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
+ end;
(*Rewrite throughout proof state. *)
fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
--- a/src/Sequents/simpdata.ML Tue Oct 18 17:59:24 2005 +0200
+++ b/src/Sequents/simpdata.ML Tue Oct 18 17:59:25 2005 +0200
@@ -235,7 +235,8 @@
(*No simprules, but basic infrastructure for simplification*)
val LK_basic_ss =
- empty_ss setsubgoaler asm_simp_tac
+ Simplifier.theory_context (the_context ()) empty_ss
+ setsubgoaler asm_simp_tac
setSSolver (mk_solver "safe" safe_solver)
setSolver (mk_solver "unsafe" unsafe_solver)
setmksimps (map mk_meta_eq o atomize o gen_all)
--- a/src/ZF/Tools/inductive_package.ML Tue Oct 18 17:59:24 2005 +0200
+++ b/src/ZF/Tools/inductive_package.ML Tue Oct 18 17:59:25 2005 +0200
@@ -339,7 +339,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 = empty_ss
+ val min_ss = Simplifier.theory_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)