# HG changeset patch
# User wenzelm
# Date 1129583413 -7200
# Node ID b9c92f38410980d341274c808137c2071f987f0c
# Parent  d810945150611b585a08813bb2bd49054647ed4b
change_claset/simpset;

diff -r d81094515061 -r b9c92f384109 src/FOL/cladata.ML
--- 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
diff -r d81094515061 -r b9c92f384109 src/HOL/Bali/AxSem.thy
--- 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
diff -r d81094515061 -r b9c92f384109 src/HOL/Bali/Basis.thy
--- 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];
diff -r d81094515061 -r b9c92f384109 src/HOL/Bali/DefiniteAssignment.thy
--- 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), 
diff -r d81094515061 -r b9c92f384109 src/HOL/Bali/Eval.thy
--- 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]
diff -r d81094515061 -r b9c92f384109 src/HOL/Bali/Evaln.thy
--- 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>)  
diff -r d81094515061 -r b9c92f384109 src/HOL/Bali/TypeSafe.thy
--- 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));
 *}
 
 
diff -r d81094515061 -r b9c92f384109 src/HOL/Bali/WellForm.thy
--- 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: 
diff -r d81094515061 -r b9c92f384109 src/HOL/Bali/WellType.thy
--- 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: 
diff -r d81094515061 -r b9c92f384109 src/HOL/Datatype.thy
--- 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
diff -r d81094515061 -r b9c92f384109 src/HOL/Hyperreal/hypreal_arith.ML
--- 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;
 
diff -r d81094515061 -r b9c92f384109 src/HOL/Library/word_setup.ML
--- 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]
diff -r d81094515061 -r b9c92f384109 src/HOL/MicroJava/Comp/CorrComp.thy
--- 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]
diff -r d81094515061 -r b9c92f384109 src/HOL/Orderings.thy
--- 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
diff -r d81094515061 -r b9c92f384109 src/HOL/Real/rat_arith.ML
--- 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;
diff -r d81094515061 -r b9c92f384109 src/HOL/Real/real_arith.ML
--- 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
diff -r d81094515061 -r b9c92f384109 src/HOL/Transitive_Closure.thy
--- 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)));
 
 *}
 
diff -r d81094515061 -r b9c92f384109 src/HOL/antisym_setup.ML
--- 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
diff -r d81094515061 -r b9c92f384109 src/HOL/cladata.ML
--- 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)];
diff -r d81094515061 -r b9c92f384109 src/HOLCF/HOLCF.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
diff -r d81094515061 -r b9c92f384109 src/HOLCF/IOA/NTP/Correctness.ML
--- 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",
diff -r d81094515061 -r b9c92f384109 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- 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));
diff -r d81094515061 -r b9c92f384109 src/HOLCF/IOA/meta_theory/TLS.ML
--- 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");
 
 
 (* ---------------------------------------------------------------- *)
diff -r d81094515061 -r b9c92f384109 src/HOLCF/IOA/meta_theory/Traces.ML
--- 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];
 
diff -r d81094515061 -r b9c92f384109 src/HOLCF/cont_proc.ML
--- 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;
diff -r d81094515061 -r b9c92f384109 src/LCF/LCF_lemmas.ML
--- 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);
diff -r d81094515061 -r b9c92f384109 src/Sequents/simpdata.ML
--- 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 *)
diff -r d81094515061 -r b9c92f384109 src/ZF/Main.ML
--- 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);
diff -r d81094515061 -r b9c92f384109 src/ZF/OrdQuant.thy
--- 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 *}
diff -r d81094515061 -r b9c92f384109 src/ZF/simpdata.ML
--- 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