# HG changeset patch
# User wenzelm
# Date 1206827749 -3600
# Node ID 49ae9456eba9ffe99901e7774de579b17511755a
# Parent  dd8996960cb0a7759813583efc39f23247d0e009
purely functional setup of claset/simpset/clasimpset;

diff -r dd8996960cb0 -r 49ae9456eba9 NEWS
--- 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'
diff -r dd8996960cb0 -r 49ae9456eba9 src/FOL/FOL.thy
--- 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
 
 
diff -r dd8996960cb0 -r 49ae9456eba9 src/FOL/cladata.ML
--- 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
diff -r dd8996960cb0 -r 49ae9456eba9 src/FOL/simpdata.ML
--- 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 ***)
diff -r dd8996960cb0 -r 49ae9456eba9 src/HOL/HOL.thy
--- 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
 *}
 
diff -r dd8996960cb0 -r 49ae9456eba9 src/HOL/Library/Word.thy
--- 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]
diff -r dd8996960cb0 -r 49ae9456eba9 src/HOL/Orderings.thy
--- 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 [
diff -r dd8996960cb0 -r 49ae9456eba9 src/HOL/Statespace/state_fun.ML
--- 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 
diff -r dd8996960cb0 -r 49ae9456eba9 src/HOL/Statespace/state_space.ML
--- 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}
diff -r dd8996960cb0 -r 49ae9456eba9 src/HOL/Tools/datatype_package.ML
--- 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 ****)
diff -r dd8996960cb0 -r 49ae9456eba9 src/HOL/Tools/record_package.ML
--- 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 *)
 
diff -r dd8996960cb0 -r 49ae9456eba9 src/HOLCF/Tools/cont_proc.ML
--- 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;
diff -r dd8996960cb0 -r 49ae9456eba9 src/ZF/Tools/typechk.ML
--- 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;