--- a/NEWS Sat Mar 29 19:24:57 2008 +0100
+++ b/NEWS Sat Mar 29 22:55:49 2008 +0100
@@ -29,8 +29,9 @@
*** Pure ***
-* Eliminated destructive theorem database. Potential INCOMPATIBILITY,
-really need to observe linear functional update of theories.
+* Eliminated destructive theorem database, simpset, claset, and
+clasimpset. Potential INCOMPATIBILITY, really need to observe linear
+update of theories within ML code.
* Commands 'use' and 'ML' are now purely functional, operating on
theory/local_theory. Removed former 'ML_setup' (on theory), use 'ML'
--- a/src/FOL/FOL.thy Sat Mar 29 19:24:57 2008 +0100
+++ b/src/FOL/FOL.thy Sat Mar 29 22:55:49 2008 +0100
@@ -293,7 +293,7 @@
setup simpsetup
setup "Simplifier.method_setup Splitter.split_modifiers"
setup Splitter.setup
-setup Clasimp.setup
+setup clasimp_setup
setup EqSubst.setup
--- a/src/FOL/cladata.ML Sat Mar 29 19:24:57 2008 +0100
+++ b/src/FOL/cladata.ML Sat Mar 29 22:55:49 2008 +0100
@@ -36,7 +36,7 @@
val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}]
addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}];
-val cla_setup = (fn thy => (change_claset_of thy (fn _ => FOL_cs); thy));
+val cla_setup = Cla.map_claset (K FOL_cs);
val case_setup =
(Method.add_methods
--- a/src/FOL/simpdata.ML Sat Mar 29 19:24:57 2008 +0100
+++ b/src/FOL/simpdata.ML Sat Mar 29 22:55:49 2008 +0100
@@ -155,7 +155,7 @@
(*classical simprules too*)
val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
-val simpsetup = (fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy));
+val simpsetup = Simplifier.map_simpset (K FOL_ss);
(*** integration of simplifier with classical reasoner ***)
--- a/src/HOL/HOL.thy Sat Mar 29 19:24:57 2008 +0100
+++ b/src/HOL/HOL.thy Sat Mar 29 22:55:49 2008 +0100
@@ -1285,9 +1285,9 @@
setup {*
Simplifier.method_setup Splitter.split_modifiers
- #> (fn thy => (change_simpset_of thy (fn _ => Simpdata.simpset_simprocs); thy))
+ #> Simplifier.map_simpset (K Simpdata.simpset_simprocs)
#> Splitter.setup
- #> Clasimp.setup
+ #> clasimp_setup
#> EqSubst.setup
*}
--- a/src/HOL/Library/Word.thy Sat Mar 29 19:24:57 2008 +0100
+++ b/src/HOL/Library/Word.thy Sat Mar 29 22:55:49 2008 +0100
@@ -2325,8 +2325,7 @@
(*lcp** val simproc1 = Simplifier.simproc thy "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f *)
val simproc2 = Simplifier.simproc @{theory} "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
in
- (fn thy => (Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [(*lcp*simproc1,*)simproc2]);
- thy))
+ Simplifier.map_simpset (fn ss => ss addsimprocs [(*lcp*simproc1,*)simproc2])
end*}
declare bv_to_nat1 [simp del]
--- a/src/HOL/Orderings.thy Sat Mar 29 19:24:57 2008 +0100
+++ b/src/HOL/Orderings.thy Sat Mar 29 22:55:49 2008 +0100
@@ -516,12 +516,12 @@
handle THM _ => NONE;
fun add_simprocs procs thy =
- (Simplifier.change_simpset_of thy (fn ss => ss
+ Simplifier.map_simpset (fn ss => ss
addsimprocs (map (fn (name, raw_ts, proc) =>
- Simplifier.simproc thy name raw_ts proc)) procs); thy);
-fun add_solver name tac thy =
- (Simplifier.change_simpset_of thy (fn ss => ss addSolver
- (mk_solver' name (fn ss => tac (MetaSimplifier.prems_of_ss ss) (MetaSimplifier.the_context ss)))); thy);
+ Simplifier.simproc thy name raw_ts proc) procs)) thy;
+fun add_solver name tac =
+ Simplifier.map_simpset (fn ss => ss addSolver
+ mk_solver' name (fn ss => tac (Simplifier.prems_of_ss ss) (Simplifier.the_context ss)));
in
add_simprocs [
--- a/src/HOL/Statespace/state_fun.ML Sat Mar 29 19:24:57 2008 +0100
+++ b/src/HOL/Statespace/state_fun.ML Sat Mar 29 22:55:49 2008 +0100
@@ -381,8 +381,7 @@
| _ => (lookup_ss addsimps [thm], ex_lookup_ss))
fun activate_simprocs ctxt =
if simprocs_active then ctxt
- else StateSpace.change_simpset
- (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt
+ else Simplifier.map_ss (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt
val ctxt' = ctxt
--- a/src/HOL/Statespace/state_space.ML Sat Mar 29 19:24:57 2008 +0100
+++ b/src/HOL/Statespace/state_space.ML Sat Mar 29 22:55:49 2008 +0100
@@ -46,9 +46,6 @@
val distinct_simproc : MetaSimplifier.simproc
- val change_simpset : (MetaSimplifier.simpset -> MetaSimplifier.simpset) ->
- Context.generic -> Context.generic
-
val get_comp : Context.generic -> string -> (Term.typ * string) Option.option
val get_silent : Context.generic -> bool
val set_silent : bool -> Context.generic -> Context.generic
@@ -247,11 +244,6 @@
| NONE => NONE)
| _ => NONE))
-fun change_simpset f =
- Context.mapping
- (fn thy => (change_simpset_of thy f; thy))
- (fn ctxt => Simplifier.put_local_simpset (f (Simplifier.get_local_simpset ctxt)) ctxt);
-
fun read_typ thy s =
Sign.read_typ thy s;
@@ -309,7 +301,7 @@
val tt' = tt |> fold upd all_names;
val activate_simproc =
Output.no_warnings
- (change_simpset (fn ss => ss addsimprocs [distinct_simproc]));
+ (Simplifier.map_ss (fn ss => ss addsimprocs [distinct_simproc]));
val ctxt' =
ctxt
|> NameSpaceData.put {declinfo=declinfo,distinctthm=tt',silent=silent}
--- a/src/HOL/Tools/datatype_package.ML Sat Mar 29 19:24:57 2008 +0100
+++ b/src/HOL/Tools/datatype_package.ML Sat Mar 29 22:55:49 2008 +0100
@@ -428,7 +428,7 @@
val simproc_setup =
Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t) #>
- (fn thy => ((change_simpset_of thy) (fn ss => ss addsimprocs [distinct_simproc]); thy));
+ Simplifier.map_simpset (fn ss => ss addsimprocs [distinct_simproc]);
(**** translation rules for case ****)
--- a/src/HOL/Tools/record_package.ML Sat Mar 29 19:24:57 2008 +0100
+++ b/src/HOL/Tools/record_package.ML Sat Mar 29 22:55:49 2008 +0100
@@ -2295,8 +2295,8 @@
val setup =
Sign.add_trfuns ([], parse_translation, [], []) #>
Sign.add_advanced_trfuns ([], adv_parse_translation, [], []) #>
- (fn thy => (Simplifier.change_simpset_of thy
- (fn ss => ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); thy));
+ Simplifier.map_simpset (fn ss =>
+ ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]);
(* outer syntax *)
--- a/src/HOLCF/Tools/cont_proc.ML Sat Mar 29 19:24:57 2008 +0100
+++ b/src/HOLCF/Tools/cont_proc.ML Sat Mar 29 22:55:49 2008 +0100
@@ -138,9 +138,6 @@
Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont;
end;
-val setup =
- (fn thy =>
- (Simplifier.change_simpset_of thy
- (fn ss => ss addsimprocs [cont_proc thy]); thy));
+fun setup thy = Simplifier.map_simpset (fn ss => ss addsimprocs [cont_proc thy]) thy;
end;
--- a/src/ZF/Tools/typechk.ML Sat Mar 29 19:24:57 2008 +0100
+++ b/src/ZF/Tools/typechk.ML Sat Mar 29 22:55:49 2008 +0100
@@ -129,6 +129,6 @@
val setup =
Attrib.add_attributes [("TC", TC_att, "declaration of type-checking rule")] #>
Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
- (fn thy => (change_simpset_of thy (fn ss => ss setSolver type_solver); thy));
+ Simplifier.map_simpset (fn ss => ss setSolver type_solver);
end;