--- a/src/FOL/FOL.thy Fri May 13 23:24:06 2011 +0200
+++ b/src/FOL/FOL.thy Fri May 13 23:58:40 2011 +0200
@@ -342,7 +342,7 @@
val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
*}
-setup {* Simplifier.map_simpset (K FOL_ss) *}
+setup {* Simplifier.map_simpset_global (K FOL_ss) *}
setup "Simplifier.method_setup Splitter.split_modifiers"
setup Splitter.setup
--- a/src/HOL/HOL.thy Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/HOL.thy Fri May 13 23:58:40 2011 +0200
@@ -1205,7 +1205,7 @@
use "Tools/simpdata.ML"
ML {* open Simpdata *}
-setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
+setup {* Simplifier.map_simpset_global (K HOL_basic_ss) *}
simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy Fri May 13 23:58:40 2011 +0200
@@ -83,7 +83,7 @@
lemma last_ind_on_first:
"l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
apply simp
- apply (tactic {* auto_tac (map_simpset_local (fn _ =>
+ apply (tactic {* auto_tac (map_simpset (fn _ =>
HOL_ss addsplits [@{thm list.split}]
addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) @{context}) *})
done
--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Fri May 13 23:58:40 2011 +0200
@@ -606,7 +606,7 @@
fun abstraction_tac ctxt =
SELECT_GOAL (auto_tac
(ctxt addSIs @{thms weak_strength_lemmas}
- |> map_simpset_local (fn ss =>
+ |> map_simpset (fn ss =>
ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}])))
*}
--- a/src/HOL/HOLCF/Tools/cont_proc.ML Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML Fri May 13 23:58:40 2011 +0200
@@ -128,6 +128,6 @@
Simplifier.simproc_global thy "cont_proc" ["cont f"] solve_cont
end
-fun setup thy = Simplifier.map_simpset (fn ss => ss addsimprocs [cont_proc thy]) thy
+fun setup thy = Simplifier.map_simpset_global (fn ss => ss addsimprocs [cont_proc thy]) thy
end
--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Fri May 13 23:58:40 2011 +0200
@@ -1202,7 +1202,7 @@
apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{context}]) *})
--{* 41 subgoals left *}
apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans},
- force_tac (map_simpset_local (fn ss => ss addsimps
+ force_tac (map_simpset (fn ss => ss addsimps
[@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *})
--{* 35 subgoals left *}
apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
@@ -1212,7 +1212,7 @@
apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *})
--{* 25 subgoals left *}
apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans},
- force_tac (map_simpset_local (fn ss => ss addsimps
+ force_tac (map_simpset (fn ss => ss addsimps
[@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *})
--{* 10 subgoals left *}
apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+
--- a/src/HOL/MicroJava/J/Conform.thy Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Fri May 13 23:58:40 2011 +0200
@@ -330,7 +330,7 @@
apply(drule conforms_heapD)
apply(tactic {*
auto_tac (put_claset HOL_cs @{context} addEs [@{thm oconf_hext}] addDs [@{thm hconfD}]
- |> map_simpset_local (fn ss => ss delsimps [@{thm split_paired_All}])) *})
+ |> map_simpset (fn ss => ss delsimps [@{thm split_paired_All}])) *})
done
lemma conforms_upd_local:
--- a/src/HOL/Orderings.thy Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Orderings.thy Fri May 13 23:58:40 2011 +0200
@@ -564,11 +564,12 @@
handle THM _ => NONE;
fun add_simprocs procs thy =
- Simplifier.map_simpset (fn ss => ss
+ Simplifier.map_simpset_global (fn ss => ss
addsimprocs (map (fn (name, raw_ts, proc) =>
Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
+
fun add_solver name tac =
- Simplifier.map_simpset (fn ss => ss addSolver
+ Simplifier.map_simpset_global (fn ss => ss addSolver
mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));
in
--- a/src/HOL/TLA/TLA.thy Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/TLA/TLA.thy Fri May 13 23:58:40 2011 +0200
@@ -599,7 +599,7 @@
*)
fun auto_inv_tac ss =
SELECT_GOAL
- (inv_tac (map_simpset_local (K ss) @{context}) 1 THEN
+ (inv_tac (map_simpset (K ss) @{context}) 1 THEN
(TRYALL (action_simp_tac
(ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
*}
--- a/src/HOL/Tools/Function/lexicographic_order.ML Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Fri May 13 23:58:40 2011 +0200
@@ -216,8 +216,7 @@
fun lexicographic_order_tac quiet ctxt =
TRY (Function_Common.apply_termination_rule ctxt 1) THEN
lex_order_tac quiet ctxt
- (auto_tac
- (map_simpset_local (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt))
+ (auto_tac (map_simpset (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt))
val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac false
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Fri May 13 23:58:40 2011 +0200
@@ -338,7 +338,7 @@
fun decomp_scnp_tac orders ctxt =
let
val extra_simps = Function_Common.Termination_Simps.get ctxt
- val autom_tac = auto_tac (map_simpset_local (fn ss => ss addsimps extra_simps) ctxt)
+ val autom_tac = auto_tac (map_simpset (fn ss => ss addsimps extra_simps) ctxt)
in
gen_sizechange_tac orders autom_tac ctxt
end
--- a/src/HOL/Tools/inductive_set.ML Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Tools/inductive_set.ML Fri May 13 23:58:40 2011 +0200
@@ -557,7 +557,7 @@
Codegen.add_preprocessor codegen_preproc #>
Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
"declaration of monotonicity rule for set operators" #>
- Context.theory_map (Simplifier.map_ss (fn ss => ss addsimprocs [collect_mem_simproc]));
+ Simplifier.map_simpset_global (fn ss => ss addsimprocs [collect_mem_simproc]);
(* outer syntax *)
--- a/src/HOL/Tools/int_arith.ML Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Tools/int_arith.ML Fri May 13 23:58:40 2011 +0200
@@ -84,8 +84,8 @@
"(m::'a::{linordered_idom,number_ring}) <= n",
"(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
-val global_setup = Simplifier.map_simpset
- (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
+val global_setup =
+ Simplifier.map_simpset_global (fn ss => ss addsimprocs [fast_int_arith_simproc]);
fun number_of thy T n =
--- a/src/HOL/Tools/recdef.ML Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Tools/recdef.ML Fri May 13 23:58:40 2011 +0200
@@ -167,7 +167,7 @@
| SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0));
val {simps, congs, wfs} = get_hints ctxt;
val ctxt' = ctxt
- |> Context.proof_map (Simplifier.map_ss (fn ss => ss addsimps simps delcongs [imp_cong]));
+ |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]);
in (ctxt', rev (map snd congs), wfs) end;
fun prepare_hints_i thy () =
@@ -175,7 +175,7 @@
val ctxt = Proof_Context.init_global thy;
val {simps, congs, wfs} = get_global_hints thy;
val ctxt' = ctxt
- |> Context.proof_map (Simplifier.map_ss (fn ss => ss addsimps simps delcongs [imp_cong]));
+ |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]);
in (ctxt', rev (map snd congs), wfs) end;
--- a/src/HOL/Tools/record.ML Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Tools/record.ML Fri May 13 23:58:40 2011 +0200
@@ -2508,8 +2508,7 @@
val setup =
Sign.add_trfuns ([], parse_translation, [], []) #>
Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
- Simplifier.map_simpset (fn ss =>
- ss addsimprocs [simproc, upd_simproc, eq_simproc]);
+ Simplifier.map_simpset_global (fn ss => ss addsimprocs [simproc, upd_simproc, eq_simproc]);
(* outer syntax *)
--- a/src/HOL/Transitive_Closure.thy Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy Fri May 13 23:58:40 2011 +0200
@@ -1027,8 +1027,8 @@
);
*}
-declaration {* fn _ =>
- Simplifier.map_ss (fn ss => ss
+setup {*
+ Simplifier.map_simpset_global (fn ss => ss
addSolver (mk_solver' "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
addSolver (mk_solver' "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
addSolver (mk_solver' "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))
--- a/src/HOL/UNITY/Comp/Alloc.thy Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy Fri May 13 23:58:40 2011 +0200
@@ -334,10 +334,10 @@
let val ctxt' =
(ctxt addIs [ext])
|> map_claset (fn cs => cs addSWrapper Record.split_wrapper)
- |> map_simpset_local (fn ss => ss
- addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
- @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
- @{thm o_apply}, @{thm Let_def}])
+ |> map_simpset (fn ss => ss addsimps
+ [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
+ @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
+ @{thm o_apply}, @{thm Let_def}])
in auto_tac ctxt' end;
*}
--- a/src/HOL/UNITY/UNITY_Main.thy Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy Fri May 13 23:58:40 2011 +0200
@@ -19,4 +19,10 @@
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
*} "for proving progress properties"
+setup {*
+ Simplifier.map_simpset_global (fn ss => ss
+ addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
+ addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}))
+*}
+
end
--- a/src/HOL/UNITY/UNITY_tactics.ML Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML Fri May 13 23:58:40 2011 +0200
@@ -59,6 +59,3 @@
th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];
-Simplifier.change_simpset (fn ss => ss
- addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
- addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}));
--- a/src/Pure/simplifier.ML Fri May 13 23:24:06 2011 +0200
+++ b/src/Pure/simplifier.ML Fri May 13 23:58:40 2011 +0200
@@ -8,12 +8,11 @@
signature BASIC_SIMPLIFIER =
sig
include BASIC_RAW_SIMPLIFIER
- val map_simpset_local: (simpset -> simpset) -> Proof.context -> Proof.context
- val change_simpset: (simpset -> simpset) -> unit
+ val map_simpset: (simpset -> simpset) -> Proof.context -> Proof.context
+ val simpset_of: Proof.context -> simpset
val global_simpset_of: theory -> simpset
val Addsimprocs: simproc list -> unit
val Delsimprocs: simproc list -> unit
- val simpset_of: Proof.context -> simpset
val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
val safe_asm_full_simp_tac: simpset -> int -> tactic
val simp_tac: simpset -> int -> tactic
@@ -31,6 +30,7 @@
signature SIMPLIFIER =
sig
include BASIC_SIMPLIFIER
+ val map_simpset_global: (simpset -> simpset) -> theory -> theory
val pretty_ss: Proof.context -> simpset -> Pretty.T
val clear_ss: simpset -> simpset
val debug_bounds: bool Unsynchronized.ref
@@ -42,10 +42,10 @@
val context: Proof.context -> simpset -> simpset
val global_context: theory -> simpset -> simpset
val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
- val simproc_global_i: theory -> string -> term list
- -> (theory -> simpset -> term -> thm option) -> simproc
- val simproc_global: theory -> string -> string list
- -> (theory -> simpset -> term -> thm option) -> simproc
+ val simproc_global_i: theory -> string -> term list ->
+ (theory -> simpset -> term -> thm option) -> simproc
+ val simproc_global: theory -> string -> string list ->
+ (theory -> simpset -> term -> thm option) -> simproc
val rewrite: simpset -> conv
val asm_rewrite: simpset -> conv
val full_rewrite: simpset -> conv
@@ -58,7 +58,6 @@
val simp_del: attribute
val cong_add: attribute
val cong_del: attribute
- val map_simpset: (simpset -> simpset) -> theory -> theory
val check_simproc: Proof.context -> xstring * Position.T -> string
val the_simproc: Proof.context -> string -> simproc
val def_simproc: {name: binding, lhss: term list,
@@ -135,26 +134,25 @@
val cong_del = attrib (op delcongs);
-(* global simpset *)
-
-fun map_simpset f = Context.theory_map (map_ss f); (* FIXME global *)
-fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
-fun global_simpset_of thy =
- Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy));
-
-fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
-fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
-
-
(* local simpset *)
-fun map_simpset_local f = Context.proof_map (map_ss f);
+fun map_simpset f = Context.proof_map (map_ss f);
fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt));
val _ = ML_Antiquote.value "simpset"
(Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())");
+(* global simpset *)
+
+fun map_simpset_global f = Context.theory_map (map_ss f);
+fun global_simpset_of thy =
+ Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy));
+
+fun Addsimprocs args = Context.>> (map_ss (fn ss => ss addsimprocs args));
+fun Delsimprocs args = Context.>> (map_ss (fn ss => ss delsimprocs args));
+
+
(** named simprocs **)
--- a/src/Sequents/LK.thy Fri May 13 23:24:06 2011 +0200
+++ b/src/Sequents/LK.thy Fri May 13 23:58:40 2011 +0200
@@ -216,6 +216,7 @@
done
use "simpdata.ML"
+setup {* Simplifier.map_simpset_global (K LK_ss) *}
text {* To create substition rules *}
--- a/src/Sequents/simpdata.ML Fri May 13 23:24:06 2011 +0200
+++ b/src/Sequents/simpdata.ML Fri May 13 23:58:40 2011 +0200
@@ -88,4 +88,3 @@
addeqcongs [@{thm left_cong}]
addcongs [@{thm imp_cong}];
-change_simpset (fn _ => LK_ss);
--- a/src/ZF/Tools/typechk.ML Fri May 13 23:24:06 2011 +0200
+++ b/src/ZF/Tools/typechk.ML Fri May 13 23:58:40 2011 +0200
@@ -130,6 +130,6 @@
val setup =
Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
typecheck_setup #>
- Simplifier.map_simpset (fn ss => ss setSolver type_solver);
+ Simplifier.map_simpset_global (fn ss => ss setSolver type_solver);
end;
--- a/src/ZF/pair.thy Fri May 13 23:24:06 2011 +0200
+++ b/src/ZF/pair.thy Fri May 13 23:58:40 2011 +0200
@@ -9,8 +9,8 @@
uses "simpdata.ML"
begin
-declaration {*
- fn _ => Simplifier.map_ss (fn ss =>
+setup {*
+ Simplifier.map_simpset_global (fn ss =>
ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
addcongs [@{thm if_weak_cong}])
*}