--- a/src/FOL/cladata.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/FOL/cladata.ML Mon Oct 17 23:10:13 2005 +0200
@@ -50,7 +50,7 @@
val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI]
addSEs [exE,alt_ex1E] addEs [allE];
-val cla_setup = [fn thy => (claset_ref_of thy := FOL_cs; thy)];
+val cla_setup = [fn thy => (change_claset_of thy (fn _ => FOL_cs); thy)];
val case_setup =
[Method.add_methods
--- a/src/HOL/Bali/AxSem.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Bali/AxSem.thy Mon Oct 17 23:10:13 2005 +0200
@@ -483,8 +483,8 @@
declare split_if [split del] split_if_asm [split del]
option.split [split del] option.split_asm [split del]
ML_setup {*
-simpset_ref() := simpset() delloop "split_all_tac";
-claset_ref () := claset () delSWrapper "split_all_tac"
+change_simpset (fn ss => ss delloop "split_all_tac");
+change_claset (fn cs => cs delSWrapper "split_all_tac");
*}
inductive "ax_derivs G" intros
--- a/src/HOL/Bali/Basis.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Bali/Basis.thy Mon Oct 17 23:10:13 2005 +0200
@@ -25,7 +25,7 @@
declare split_if_asm [split] option.split [split] option.split_asm [split]
ML {*
-simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
+change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
*}
declare if_weak_cong [cong del] option.weak_case_cong [cong del]
declare length_Suc_conv [iff];
--- a/src/HOL/Bali/DefiniteAssignment.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Mon Oct 17 23:10:13 2005 +0200
@@ -830,7 +830,7 @@
declare assigns_if.simps [simp del]
declare split_paired_All [simp del] split_paired_Ex [simp del]
ML_setup {*
-simpset_ref() := simpset() delloop "split_all_tac"
+change_simpset (fn ss => ss delloop "split_all_tac");
*}
inductive_cases da_elim_cases [cases set]:
"Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"
@@ -897,7 +897,7 @@
declare assigns_if.simps [simp]
declare split_paired_All [simp] split_paired_Ex [simp]
ML_setup {*
-simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
+change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
*}
(* To be able to eliminate both the versions with the overloaded brackets:
(B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A) and with the explicit constructor (B \<guillemotright>In1r Skip\<guillemotright> A),
--- a/src/HOL/Bali/Eval.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Bali/Eval.thy Mon Oct 17 23:10:13 2005 +0200
@@ -831,7 +831,7 @@
declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
declare split_paired_All [simp del] split_paired_Ex [simp del]
ML_setup {*
-simpset_ref() := simpset() delloop "split_all_tac"
+change_simpset (fn ss => ss delloop "split_all_tac");
*}
inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'"
@@ -870,7 +870,7 @@
declare not_None_eq [simp] (* IntDef.Zero_def [simp] *)
declare split_paired_All [simp] split_paired_Ex [simp]
ML_setup {*
-simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
+change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
*}
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
--- a/src/HOL/Bali/Evaln.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Bali/Evaln.thy Mon Oct 17 23:10:13 2005 +0200
@@ -227,7 +227,7 @@
not_None_eq [simp del]
split_paired_All [simp del] split_paired_Ex [simp del]
ML_setup {*
-simpset_ref() := simpset() delloop "split_all_tac"
+change_simpset (fn ss => ss delloop "split_all_tac");
*}
inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> vs'"
@@ -270,7 +270,7 @@
not_None_eq [simp]
split_paired_All [simp] split_paired_Ex [simp]
ML_setup {*
-simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
+change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
*}
lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>
(case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)
--- a/src/HOL/Bali/TypeSafe.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Mon Oct 17 23:10:13 2005 +0200
@@ -730,8 +730,8 @@
declare split_if [split del] split_if_asm [split del]
option.split [split del] option.split_asm [split del]
ML_setup {*
-simpset_ref() := simpset() delloop "split_all_tac";
-claset_ref () := claset () delSWrapper "split_all_tac"
+change_simpset (fn ss => ss delloop "split_all_tac");
+change_claset (fn cs => cs delSWrapper "split_all_tac");
*}
lemma FVar_lemma:
"\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2);
@@ -760,8 +760,8 @@
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
ML_setup {*
-claset_ref() := claset() addSbefore ("split_all_tac", split_all_tac);
-simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
+change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
+change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
*}
@@ -878,8 +878,8 @@
declare split_if [split del] split_if_asm [split del]
option.split [split del] option.split_asm [split del]
ML_setup {*
-simpset_ref() := simpset() delloop "split_all_tac";
-claset_ref () := claset () delSWrapper "split_all_tac"
+change_simpset (fn ss => ss delloop "split_all_tac");
+change_claset (fn cs => cs delSWrapper "split_all_tac");
*}
lemma conforms_init_lvars:
"\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;
@@ -932,8 +932,8 @@
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
ML_setup {*
-claset_ref() := claset() addSbefore ("split_all_tac", split_all_tac);
-simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
+change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
+change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
*}
--- a/src/HOL/Bali/WellForm.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Bali/WellForm.thy Mon Oct 17 23:10:13 2005 +0200
@@ -2178,8 +2178,8 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
ML_setup {*
-simpset_ref() := simpset() delloop "split_all_tac";
-claset_ref () := claset () delSWrapper "split_all_tac"
+change_simpset (fn ss => ss delloop "split_all_tac");
+change_claset (fn cs => cs delSWrapper "split_all_tac");
*}
lemma dynamic_mheadsD:
"\<lbrakk>emh \<in> mheads G S statT sig;
@@ -2309,8 +2309,8 @@
qed
declare split_paired_All [simp] split_paired_Ex [simp]
ML_setup {*
-claset_ref() := claset() addSbefore ("split_all_tac", split_all_tac);
-simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
+change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
+change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
*}
(* Tactical version *)
@@ -2455,8 +2455,8 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
ML_setup {*
-simpset_ref() := simpset() delloop "split_all_tac";
-claset_ref () := claset () delSWrapper "split_all_tac"
+change_simpset (fn ss => ss delloop "split_all_tac");
+change_claset (fn cs => cs delSWrapper "split_all_tac");
*}
lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow> wf_prog (prg E) \<longrightarrow>
dt=empty_dt \<longrightarrow> (case T of
@@ -2481,8 +2481,8 @@
done
declare split_paired_All [simp] split_paired_Ex [simp]
ML_setup {*
-claset_ref() := claset() addSbefore ("split_all_tac", split_all_tac);
-simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
+change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
+change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
*}
lemma ty_expr_is_type:
--- a/src/HOL/Bali/WellType.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Bali/WellType.thy Mon Oct 17 23:10:13 2005 +0200
@@ -469,7 +469,7 @@
declare split_if [split del] split_if_asm [split del]
declare split_paired_All [simp del] split_paired_Ex [simp del]
ML_setup {*
-simpset_ref() := simpset() delloop "split_all_tac"
+change_simpset (fn ss => ss delloop "split_all_tac")
*}
inductive_cases wt_elim_cases [cases set]:
@@ -507,7 +507,7 @@
declare split_if [split] split_if_asm [split]
declare split_paired_All [simp] split_paired_Ex [simp]
ML_setup {*
-simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
+change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
*}
lemma is_acc_class_is_accessible:
--- a/src/HOL/Datatype.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Datatype.thy Mon Oct 17 23:10:13 2005 +0200
@@ -169,7 +169,7 @@
lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
by simp
-ML_setup {* claset_ref() := claset() addSD2 ("ospec", thm "ospec") *}
+ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *}
lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
by (cases xo) auto
--- a/src/HOL/Hyperreal/hypreal_arith.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Hyperreal/hypreal_arith.ML Mon Oct 17 23:10:13 2005 +0200
@@ -36,7 +36,7 @@
neqE = neqE,
simpset = simpset}),
arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT),
- Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]];
+ fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]); thy)];
end;
--- a/src/HOL/Library/word_setup.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Library/word_setup.ML Mon Oct 17 23:10:13 2005 +0200
@@ -38,7 +38,8 @@
(*lcp** val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of ?w)"] f ***)
val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (?x # ?xs)"] g
in
- Simplifier.change_simpset_of (op addsimprocs) [(*lcp*simproc1,**)simproc2] thy
+ Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [(*lcp*simproc1,**)simproc2]);
+ thy
end
in
val setup_word = [add_word]
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy Mon Oct 17 23:10:13 2005 +0200
@@ -477,7 +477,7 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
ML_setup {*
-simpset_ref() := simpset() delloop "split_all_tac"
+change_simpset (fn ss => ss delloop "split_all_tac");
*}
lemma distinct_method: "\<lbrakk> wf_java_prog G; is_class G C;
@@ -1266,7 +1266,7 @@
(* reinstall pair splits *)
declare split_paired_All [simp] split_paired_Ex [simp]
ML_setup {*
-simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
+change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
*}
declare wf_prog_ws_prog [simp del]
--- a/src/HOL/Orderings.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Orderings.thy Mon Oct 17 23:10:13 2005 +0200
@@ -363,9 +363,9 @@
end); (* struct *)
-simpset_ref() := simpset ()
+change_simpset (fn ss => ss
addSolver (mk_solver "Trans_linear" (fn _ => Order_Tac.linear_tac))
- addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac));
+ addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac)));
(* Adding the transitivity reasoners also as safe solvers showed a slight
speed up, but the reasoning strength appears to be not higher (at least
no breaking of additional proofs in the entire HOL distribution, as
--- a/src/HOL/Real/rat_arith.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Real/rat_arith.ML Mon Oct 17 23:10:13 2005 +0200
@@ -49,6 +49,6 @@
addsimprocs simprocs}),
arith_inj_const("IntDef.of_nat", HOLogic.natT --> ratT),
arith_inj_const("IntDef.of_int", HOLogic.intT --> ratT),
- Simplifier.change_simpset_of (op addsimprocs) [fast_rat_arith_simproc]];
+ fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_rat_arith_simproc]); thy)];
end;
--- a/src/HOL/Real/real_arith.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Real/real_arith.ML Mon Oct 17 23:10:13 2005 +0200
@@ -127,7 +127,7 @@
simpset = simpset addsimps simps}),
arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT),
arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT),
- Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]];
+ fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_real_arith_simproc]); thy)];
(* some thms for injection nat => real:
real_of_nat_zero
--- a/src/HOL/Transitive_Closure.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Transitive_Closure.thy Mon Oct 17 23:10:13 2005 +0200
@@ -489,9 +489,9 @@
end); (* struct *)
-simpset_ref() := simpset ()
- addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
- addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac));
+change_simpset (fn ss => ss
+ addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
+ addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac)));
*}
--- a/src/HOL/antisym_setup.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/antisym_setup.ML Mon Oct 17 23:10:13 2005 +0200
@@ -48,6 +48,7 @@
in
val antisym_setup =
- [Simplifier.change_simpset_of (op addsimprocs) [antisym_le,antisym_less]];
+ [fn thy => (Simplifier.change_simpset_of thy
+ (fn ss => ss addsimprocs [antisym_le, antisym_less]); thy)]
end
--- a/src/HOL/cladata.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/cladata.ML Mon Oct 17 23:10:13 2005 +0200
@@ -70,4 +70,4 @@
val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, the_equality]
addSEs [exE] addEs [allE];
-val clasetup = [fn thy => (claset_ref_of thy := HOL_cs; thy)];
+val clasetup = [fn thy => (change_claset_of thy (fn _ => HOL_cs); thy)];
--- a/src/HOLCF/HOLCF.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOLCF/HOLCF.thy Mon Oct 17 23:10:13 2005 +0200
@@ -21,9 +21,9 @@
begin
ML_setup {*
- simpset_ref() := simpset() addSolver
+ change_simpset (fn simpset => simpset addSolver
(mk_solver' "adm_tac" (fn ss =>
- adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss)));
+ adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
*}
end
--- a/src/HOLCF/IOA/NTP/Correctness.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.ML Mon Oct 17 23:10:13 2005 +0200
@@ -4,7 +4,7 @@
*)
(* repeated from Traces.ML *)
-claset_ref() := claset() delSWrapper "split_all_tac";
+change_claset (fn cs => cs delSWrapper "split_all_tac");
val hom_ioas = [thm "Spec.ioa_def", thm "Spec.trans_def",
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Mon Oct 17 23:10:13 2005 +0200
@@ -3,7 +3,7 @@
Author: Olaf Müller
*)
-simpset_ref () := simpset() setmksym (K NONE);
+change_simpset (fn ss => ss setmksym (K NONE));
(* ---------------------------------------------------------------- *)
section "mksch rewrite rules";
@@ -1223,4 +1223,4 @@
qed"compositionality_tr_modules";
-simpset_ref () := simpset() setmksym (SOME o symmetric_fun);
+change_simpset (fn ss => ss setmksym (SOME o symmetric_fun));
--- a/src/HOLCF/IOA/meta_theory/TLS.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/TLS.ML Mon Oct 17 23:10:13 2005 +0200
@@ -7,7 +7,7 @@
Delsimps (ex_simps @ all_simps);
Delsimps [split_paired_Ex];
Addsimps [Let_def];
-claset_ref() := claset() delSWrapper "split_all_tac";
+change_claset (fn cs => cs delSWrapper "split_all_tac");
(* ---------------------------------------------------------------- *)
--- a/src/HOLCF/IOA/meta_theory/Traces.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Mon Oct 17 23:10:13 2005 +0200
@@ -9,7 +9,7 @@
Delsimps (ex_simps @ all_simps);
Delsimps [split_paired_Ex];
Addsimps [Let_def];
-claset_ref() := claset() delSWrapper "split_all_tac";
+change_claset (fn cs => cs delSWrapper "split_all_tac");
val exec_rws = [executions_def,is_exec_frag_def];
--- a/src/HOLCF/cont_proc.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOLCF/cont_proc.ML Mon Oct 17 23:10:13 2005 +0200
@@ -110,6 +110,6 @@
end;
val setup =
- [fn thy => Simplifier.change_simpset_of (op addsimprocs) [cont_proc thy] thy];
+ [fn thy => (Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [cont_proc thy]); thy)];
end;
--- a/src/LCF/LCF_lemmas.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/LCF/LCF_lemmas.ML Mon Oct 17 23:10:13 2005 +0200
@@ -92,3 +92,5 @@
not_FF_eq_UU,not_FF_eq_TT,
COND_UU,COND_TT,COND_FF,
surj_pairing,FST,SND];
+
+change_simpset (fn _ => LCF_ss);
--- a/src/Sequents/simpdata.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/Sequents/simpdata.ML Mon Oct 17 23:10:13 2005 +0200
@@ -223,8 +223,6 @@
qed "if_not_P";
-open Simplifier;
-
(*** Standard simpsets ***)
val triv_rls = [FalseL, TrueR, basic, refl, iff_refl, reflexive_thm];
@@ -259,7 +257,7 @@
addeqcongs [left_cong]
addcongs [imp_cong];
-simpset_ref() := LK_ss;
+change_simpset (fn _ => LK_ss);
(* To create substition rules *)
--- a/src/ZF/Main.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/ZF/Main.ML Mon Oct 17 23:10:13 2005 +0200
@@ -1,7 +1,7 @@
+
+(* $Id$ *)
structure Main =
struct
val thy = the_context ();
end;
-
-simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
--- a/src/ZF/OrdQuant.thy Mon Oct 17 23:10:10 2005 +0200
+++ b/src/ZF/OrdQuant.thy Mon Oct 17 23:10:13 2005 +0200
@@ -392,7 +392,7 @@
atomize ([("OrdQuant.oall", [ospec]),("OrdQuant.rall", [rspec])]@
ZF_conn_pairs,
ZF_mem_pairs);
-simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
+change_simpset (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all));
*}
text {* Setting up the one-point-rule simproc *}
--- a/src/ZF/simpdata.ML Mon Oct 17 23:10:10 2005 +0200
+++ b/src/ZF/simpdata.ML Mon Oct 17 23:10:13 2005 +0200
@@ -48,10 +48,10 @@
val type_solver =
mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems));
-simpset_ref() :=
- simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
+change_simpset (fn ss =>
+ ss setmksimps (map mk_eq o ZF_atomize o gen_all)
addcongs [if_weak_cong]
- setSolver type_solver;
+ setSolver type_solver);
local