change_claset/simpset;
authorwenzelm
Mon Oct 17 23:10:13 2005 +0200 (2005-10-17)
changeset 17876b9c92f384109
parent 17875 d81094515061
child 17877 67d5ab1cb0d8
change_claset/simpset;
src/FOL/cladata.ML
src/HOL/Bali/AxSem.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/DefiniteAssignment.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Bali/WellForm.thy
src/HOL/Bali/WellType.thy
src/HOL/Datatype.thy
src/HOL/Hyperreal/hypreal_arith.ML
src/HOL/Library/word_setup.ML
src/HOL/MicroJava/Comp/CorrComp.thy
src/HOL/Orderings.thy
src/HOL/Real/rat_arith.ML
src/HOL/Real/real_arith.ML
src/HOL/Transitive_Closure.thy
src/HOL/antisym_setup.ML
src/HOL/cladata.ML
src/HOLCF/HOLCF.thy
src/HOLCF/IOA/NTP/Correctness.ML
src/HOLCF/IOA/meta_theory/CompoTraces.ML
src/HOLCF/IOA/meta_theory/TLS.ML
src/HOLCF/IOA/meta_theory/Traces.ML
src/HOLCF/cont_proc.ML
src/LCF/LCF_lemmas.ML
src/Sequents/simpdata.ML
src/ZF/Main.ML
src/ZF/OrdQuant.thy
src/ZF/simpdata.ML
     1.1 --- a/src/FOL/cladata.ML	Mon Oct 17 23:10:10 2005 +0200
     1.2 +++ b/src/FOL/cladata.ML	Mon Oct 17 23:10:13 2005 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4  val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
     1.5                       addSEs [exE,alt_ex1E] addEs [allE];
     1.6  
     1.7 -val cla_setup = [fn thy => (claset_ref_of thy := FOL_cs; thy)];
     1.8 +val cla_setup = [fn thy => (change_claset_of thy (fn _ => FOL_cs); thy)];
     1.9  
    1.10  val case_setup =
    1.11   [Method.add_methods
     2.1 --- a/src/HOL/Bali/AxSem.thy	Mon Oct 17 23:10:10 2005 +0200
     2.2 +++ b/src/HOL/Bali/AxSem.thy	Mon Oct 17 23:10:13 2005 +0200
     2.3 @@ -483,8 +483,8 @@
     2.4  declare split_if     [split del] split_if_asm     [split del] 
     2.5          option.split [split del] option.split_asm [split del]
     2.6  ML_setup {*
     2.7 -simpset_ref() := simpset() delloop "split_all_tac";
     2.8 -claset_ref () := claset () delSWrapper "split_all_tac"
     2.9 +change_simpset (fn ss => ss delloop "split_all_tac");
    2.10 +change_claset (fn cs => cs delSWrapper "split_all_tac");
    2.11  *}
    2.12  
    2.13  inductive "ax_derivs G" intros
     3.1 --- a/src/HOL/Bali/Basis.thy	Mon Oct 17 23:10:10 2005 +0200
     3.2 +++ b/src/HOL/Bali/Basis.thy	Mon Oct 17 23:10:13 2005 +0200
     3.3 @@ -25,7 +25,7 @@
     3.4  
     3.5  declare split_if_asm  [split] option.split [split] option.split_asm [split]
     3.6  ML {*
     3.7 -simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
     3.8 +change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
     3.9  *}
    3.10  declare if_weak_cong [cong del] option.weak_case_cong [cong del]
    3.11  declare length_Suc_conv [iff];
     4.1 --- a/src/HOL/Bali/DefiniteAssignment.thy	Mon Oct 17 23:10:10 2005 +0200
     4.2 +++ b/src/HOL/Bali/DefiniteAssignment.thy	Mon Oct 17 23:10:13 2005 +0200
     4.3 @@ -830,7 +830,7 @@
     4.4  declare assigns_if.simps [simp del]
     4.5  declare split_paired_All [simp del] split_paired_Ex [simp del]
     4.6  ML_setup {*
     4.7 -simpset_ref() := simpset() delloop "split_all_tac"
     4.8 +change_simpset (fn ss => ss delloop "split_all_tac");
     4.9  *}
    4.10  inductive_cases da_elim_cases [cases set]:
    4.11    "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A" 
    4.12 @@ -897,7 +897,7 @@
    4.13  declare assigns_if.simps [simp]
    4.14  declare split_paired_All [simp] split_paired_Ex [simp]
    4.15  ML_setup {*
    4.16 -simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    4.17 +change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    4.18  *}
    4.19  (* To be able to eliminate both the versions with the overloaded brackets: 
    4.20     (B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A) and with the explicit constructor (B \<guillemotright>In1r Skip\<guillemotright> A), 
     5.1 --- a/src/HOL/Bali/Eval.thy	Mon Oct 17 23:10:10 2005 +0200
     5.2 +++ b/src/HOL/Bali/Eval.thy	Mon Oct 17 23:10:13 2005 +0200
     5.3 @@ -831,7 +831,7 @@
     5.4  declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
     5.5  declare split_paired_All [simp del] split_paired_Ex [simp del]
     5.6  ML_setup {*
     5.7 -simpset_ref() := simpset() delloop "split_all_tac"
     5.8 +change_simpset (fn ss => ss delloop "split_all_tac");
     5.9  *}
    5.10  inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'"
    5.11  
    5.12 @@ -870,7 +870,7 @@
    5.13  declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
    5.14  declare split_paired_All [simp] split_paired_Ex [simp]
    5.15  ML_setup {*
    5.16 -simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    5.17 +change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    5.18  *}
    5.19  declare split_if     [split] split_if_asm     [split] 
    5.20          option.split [split] option.split_asm [split]
     6.1 --- a/src/HOL/Bali/Evaln.thy	Mon Oct 17 23:10:10 2005 +0200
     6.2 +++ b/src/HOL/Bali/Evaln.thy	Mon Oct 17 23:10:13 2005 +0200
     6.3 @@ -227,7 +227,7 @@
     6.4          not_None_eq [simp del] 
     6.5          split_paired_All [simp del] split_paired_Ex [simp del]
     6.6  ML_setup {*
     6.7 -simpset_ref() := simpset() delloop "split_all_tac"
     6.8 +change_simpset (fn ss => ss delloop "split_all_tac");
     6.9  *}
    6.10  inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> vs'"
    6.11  
    6.12 @@ -270,7 +270,7 @@
    6.13          not_None_eq [simp] 
    6.14          split_paired_All [simp] split_paired_Ex [simp]
    6.15  ML_setup {*
    6.16 -simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    6.17 +change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    6.18  *}
    6.19  lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>  
    6.20    (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)  
     7.1 --- a/src/HOL/Bali/TypeSafe.thy	Mon Oct 17 23:10:10 2005 +0200
     7.2 +++ b/src/HOL/Bali/TypeSafe.thy	Mon Oct 17 23:10:13 2005 +0200
     7.3 @@ -730,8 +730,8 @@
     7.4  declare split_if     [split del] split_if_asm     [split del] 
     7.5          option.split [split del] option.split_asm [split del]
     7.6  ML_setup {*
     7.7 -simpset_ref() := simpset() delloop "split_all_tac";
     7.8 -claset_ref () := claset () delSWrapper "split_all_tac"
     7.9 +change_simpset (fn ss => ss delloop "split_all_tac");
    7.10 +change_claset (fn cs => cs delSWrapper "split_all_tac");
    7.11  *}
    7.12  lemma FVar_lemma: 
    7.13  "\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2); 
    7.14 @@ -760,8 +760,8 @@
    7.15  declare split_if     [split] split_if_asm     [split] 
    7.16          option.split [split] option.split_asm [split]
    7.17  ML_setup {*
    7.18 -claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
    7.19 -simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    7.20 +change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
    7.21 +change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    7.22  *}
    7.23  
    7.24  
    7.25 @@ -878,8 +878,8 @@
    7.26  declare split_if     [split del] split_if_asm     [split del] 
    7.27          option.split [split del] option.split_asm [split del]
    7.28  ML_setup {*
    7.29 -simpset_ref() := simpset() delloop "split_all_tac";
    7.30 -claset_ref () := claset () delSWrapper "split_all_tac"
    7.31 +change_simpset (fn ss => ss delloop "split_all_tac");
    7.32 +change_claset (fn cs => cs delSWrapper "split_all_tac");
    7.33  *}
    7.34  lemma conforms_init_lvars: 
    7.35  "\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;  
    7.36 @@ -932,8 +932,8 @@
    7.37  declare split_if     [split] split_if_asm     [split] 
    7.38          option.split [split] option.split_asm [split]
    7.39  ML_setup {*
    7.40 -claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
    7.41 -simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    7.42 +change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
    7.43 +change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    7.44  *}
    7.45  
    7.46  
     8.1 --- a/src/HOL/Bali/WellForm.thy	Mon Oct 17 23:10:10 2005 +0200
     8.2 +++ b/src/HOL/Bali/WellForm.thy	Mon Oct 17 23:10:13 2005 +0200
     8.3 @@ -2178,8 +2178,8 @@
     8.4  
     8.5  declare split_paired_All [simp del] split_paired_Ex [simp del]
     8.6  ML_setup {*
     8.7 -simpset_ref() := simpset() delloop "split_all_tac";
     8.8 -claset_ref () := claset () delSWrapper "split_all_tac"
     8.9 +change_simpset (fn ss => ss delloop "split_all_tac");
    8.10 +change_claset (fn cs => cs delSWrapper "split_all_tac");
    8.11  *}
    8.12  lemma dynamic_mheadsD:   
    8.13  "\<lbrakk>emh \<in> mheads G S statT sig;    
    8.14 @@ -2309,8 +2309,8 @@
    8.15  qed
    8.16  declare split_paired_All [simp] split_paired_Ex [simp]
    8.17  ML_setup {*
    8.18 -claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
    8.19 -simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    8.20 +change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
    8.21 +change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    8.22  *}
    8.23  
    8.24  (* Tactical version *)
    8.25 @@ -2455,8 +2455,8 @@
    8.26  
    8.27  declare split_paired_All [simp del] split_paired_Ex [simp del]
    8.28  ML_setup {*
    8.29 -simpset_ref() := simpset() delloop "split_all_tac";
    8.30 -claset_ref () := claset () delSWrapper "split_all_tac"
    8.31 +change_simpset (fn ss => ss delloop "split_all_tac");
    8.32 +change_claset (fn cs => cs delSWrapper "split_all_tac");
    8.33  *}
    8.34  lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow>  wf_prog (prg E) \<longrightarrow> 
    8.35    dt=empty_dt \<longrightarrow> (case T of 
    8.36 @@ -2481,8 +2481,8 @@
    8.37  done
    8.38  declare split_paired_All [simp] split_paired_Ex [simp]
    8.39  ML_setup {*
    8.40 -claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
    8.41 -simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    8.42 +change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
    8.43 +change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    8.44  *}
    8.45  
    8.46  lemma ty_expr_is_type: 
     9.1 --- a/src/HOL/Bali/WellType.thy	Mon Oct 17 23:10:10 2005 +0200
     9.2 +++ b/src/HOL/Bali/WellType.thy	Mon Oct 17 23:10:13 2005 +0200
     9.3 @@ -469,7 +469,7 @@
     9.4  declare split_if [split del] split_if_asm [split del]
     9.5  declare split_paired_All [simp del] split_paired_Ex [simp del]
     9.6  ML_setup {*
     9.7 -simpset_ref() := simpset() delloop "split_all_tac"
     9.8 +change_simpset (fn ss => ss delloop "split_all_tac")
     9.9  *}
    9.10  
    9.11  inductive_cases wt_elim_cases [cases set]:
    9.12 @@ -507,7 +507,7 @@
    9.13  declare split_if [split] split_if_asm [split]
    9.14  declare split_paired_All [simp] split_paired_Ex [simp]
    9.15  ML_setup {*
    9.16 -simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    9.17 +change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    9.18  *}
    9.19  
    9.20  lemma is_acc_class_is_accessible: 
    10.1 --- a/src/HOL/Datatype.thy	Mon Oct 17 23:10:10 2005 +0200
    10.2 +++ b/src/HOL/Datatype.thy	Mon Oct 17 23:10:13 2005 +0200
    10.3 @@ -169,7 +169,7 @@
    10.4  lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
    10.5    by simp
    10.6  
    10.7 -ML_setup {* claset_ref() := claset() addSD2 ("ospec", thm "ospec") *}
    10.8 +ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *}
    10.9  
   10.10  lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
   10.11    by (cases xo) auto
    11.1 --- a/src/HOL/Hyperreal/hypreal_arith.ML	Mon Oct 17 23:10:10 2005 +0200
    11.2 +++ b/src/HOL/Hyperreal/hypreal_arith.ML	Mon Oct 17 23:10:13 2005 +0200
    11.3 @@ -36,7 +36,7 @@
    11.4      neqE = neqE,
    11.5      simpset = simpset}),
    11.6    arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT),
    11.7 -  Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]];
    11.8 +  fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]); thy)];
    11.9  
   11.10  end;
   11.11  
    12.1 --- a/src/HOL/Library/word_setup.ML	Mon Oct 17 23:10:10 2005 +0200
    12.2 +++ b/src/HOL/Library/word_setup.ML	Mon Oct 17 23:10:13 2005 +0200
    12.3 @@ -38,7 +38,8 @@
    12.4    (*lcp**	    val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of ?w)"] f ***)
    12.5  	    val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (?x # ?xs)"] g
    12.6  	in
    12.7 -	    Simplifier.change_simpset_of (op addsimprocs) [(*lcp*simproc1,**)simproc2] thy
    12.8 +	  Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [(*lcp*simproc1,**)simproc2]);
    12.9 +          thy
   12.10  	end
   12.11  in
   12.12  val setup_word = [add_word]
    13.1 --- a/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Oct 17 23:10:10 2005 +0200
    13.2 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Oct 17 23:10:13 2005 +0200
    13.3 @@ -477,7 +477,7 @@
    13.4  
    13.5  declare split_paired_All [simp del] split_paired_Ex [simp del]
    13.6  ML_setup {*
    13.7 -simpset_ref() := simpset() delloop "split_all_tac"
    13.8 +change_simpset (fn ss => ss delloop "split_all_tac");
    13.9  *}
   13.10  
   13.11  lemma distinct_method: "\<lbrakk> wf_java_prog G; is_class G C; 
   13.12 @@ -1266,7 +1266,7 @@
   13.13  (* reinstall pair splits *)
   13.14  declare split_paired_All [simp] split_paired_Ex [simp]
   13.15  ML_setup {*
   13.16 -simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
   13.17 +change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
   13.18  *}
   13.19  
   13.20  declare wf_prog_ws_prog [simp del]
    14.1 --- a/src/HOL/Orderings.thy	Mon Oct 17 23:10:10 2005 +0200
    14.2 +++ b/src/HOL/Orderings.thy	Mon Oct 17 23:10:13 2005 +0200
    14.3 @@ -363,9 +363,9 @@
    14.4  
    14.5    end);  (* struct *)
    14.6  
    14.7 -simpset_ref() := simpset ()
    14.8 +change_simpset (fn ss => ss
    14.9      addSolver (mk_solver "Trans_linear" (fn _ => Order_Tac.linear_tac))
   14.10 -    addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac));
   14.11 +    addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac)));
   14.12    (* Adding the transitivity reasoners also as safe solvers showed a slight
   14.13       speed up, but the reasoning strength appears to be not higher (at least
   14.14       no breaking of additional proofs in the entire HOL distribution, as
    15.1 --- a/src/HOL/Real/rat_arith.ML	Mon Oct 17 23:10:10 2005 +0200
    15.2 +++ b/src/HOL/Real/rat_arith.ML	Mon Oct 17 23:10:13 2005 +0200
    15.3 @@ -49,6 +49,6 @@
    15.4                        addsimprocs simprocs}),
    15.5    arith_inj_const("IntDef.of_nat", HOLogic.natT --> ratT),
    15.6    arith_inj_const("IntDef.of_int", HOLogic.intT --> ratT),
    15.7 -  Simplifier.change_simpset_of (op addsimprocs) [fast_rat_arith_simproc]];
    15.8 +  fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_rat_arith_simproc]); thy)];
    15.9  
   15.10  end;
    16.1 --- a/src/HOL/Real/real_arith.ML	Mon Oct 17 23:10:10 2005 +0200
    16.2 +++ b/src/HOL/Real/real_arith.ML	Mon Oct 17 23:10:13 2005 +0200
    16.3 @@ -127,7 +127,7 @@
    16.4      simpset = simpset addsimps simps}),
    16.5    arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT),
    16.6    arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT),
    16.7 -  Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]];
    16.8 +  fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_real_arith_simproc]); thy)];
    16.9  
   16.10  (* some thms for injection nat => real:
   16.11  real_of_nat_zero
    17.1 --- a/src/HOL/Transitive_Closure.thy	Mon Oct 17 23:10:10 2005 +0200
    17.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Oct 17 23:10:13 2005 +0200
    17.3 @@ -489,9 +489,9 @@
    17.4    
    17.5    end); (* struct *)
    17.6  
    17.7 -simpset_ref() := simpset ()
    17.8 -    addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
    17.9 -    addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac));
   17.10 +change_simpset (fn ss => ss
   17.11 +  addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
   17.12 +  addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac)));
   17.13  
   17.14  *}
   17.15  
    18.1 --- a/src/HOL/antisym_setup.ML	Mon Oct 17 23:10:10 2005 +0200
    18.2 +++ b/src/HOL/antisym_setup.ML	Mon Oct 17 23:10:13 2005 +0200
    18.3 @@ -48,6 +48,7 @@
    18.4  in
    18.5  
    18.6  val antisym_setup =
    18.7 - [Simplifier.change_simpset_of (op addsimprocs) [antisym_le,antisym_less]];
    18.8 + [fn thy => (Simplifier.change_simpset_of thy
    18.9 +  (fn ss => ss addsimprocs [antisym_le, antisym_less]); thy)]
   18.10  
   18.11  end
    19.1 --- a/src/HOL/cladata.ML	Mon Oct 17 23:10:10 2005 +0200
    19.2 +++ b/src/HOL/cladata.ML	Mon Oct 17 23:10:13 2005 +0200
    19.3 @@ -70,4 +70,4 @@
    19.4  val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, the_equality] 
    19.5                       addSEs [exE] addEs [allE];
    19.6  
    19.7 -val clasetup = [fn thy => (claset_ref_of thy := HOL_cs; thy)];
    19.8 +val clasetup = [fn thy => (change_claset_of thy (fn _ => HOL_cs); thy)];
    20.1 --- a/src/HOLCF/HOLCF.thy	Mon Oct 17 23:10:10 2005 +0200
    20.2 +++ b/src/HOLCF/HOLCF.thy	Mon Oct 17 23:10:13 2005 +0200
    20.3 @@ -21,9 +21,9 @@
    20.4  begin
    20.5  
    20.6  ML_setup {*
    20.7 -  simpset_ref() := simpset() addSolver
    20.8 +  change_simpset (fn simpset => simpset addSolver
    20.9      (mk_solver' "adm_tac" (fn ss =>
   20.10 -      adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss)));
   20.11 +      adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
   20.12  *}
   20.13  
   20.14  end
    21.1 --- a/src/HOLCF/IOA/NTP/Correctness.ML	Mon Oct 17 23:10:10 2005 +0200
    21.2 +++ b/src/HOLCF/IOA/NTP/Correctness.ML	Mon Oct 17 23:10:13 2005 +0200
    21.3 @@ -4,7 +4,7 @@
    21.4  *)
    21.5  
    21.6  (* repeated from Traces.ML *)
    21.7 -claset_ref() := claset() delSWrapper "split_all_tac";
    21.8 +change_claset (fn cs => cs delSWrapper "split_all_tac");
    21.9  
   21.10  
   21.11  val hom_ioas = [thm "Spec.ioa_def", thm "Spec.trans_def",
    22.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Mon Oct 17 23:10:10 2005 +0200
    22.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Mon Oct 17 23:10:13 2005 +0200
    22.3 @@ -3,7 +3,7 @@
    22.4      Author:     Olaf Müller
    22.5  *)
    22.6  
    22.7 -simpset_ref () := simpset() setmksym (K NONE);
    22.8 +change_simpset (fn ss => ss setmksym (K NONE));
    22.9  
   22.10  (* ---------------------------------------------------------------- *)
   22.11                     section "mksch rewrite rules";
   22.12 @@ -1223,4 +1223,4 @@
   22.13  qed"compositionality_tr_modules";
   22.14  
   22.15  
   22.16 -simpset_ref () := simpset() setmksym (SOME o symmetric_fun);
   22.17 +change_simpset (fn ss => ss setmksym (SOME o symmetric_fun));
    23.1 --- a/src/HOLCF/IOA/meta_theory/TLS.ML	Mon Oct 17 23:10:10 2005 +0200
    23.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Mon Oct 17 23:10:13 2005 +0200
    23.3 @@ -7,7 +7,7 @@
    23.4  Delsimps (ex_simps @ all_simps);
    23.5  Delsimps [split_paired_Ex];
    23.6  Addsimps [Let_def];
    23.7 -claset_ref() := claset() delSWrapper "split_all_tac";
    23.8 +change_claset (fn cs => cs delSWrapper "split_all_tac");
    23.9  
   23.10  
   23.11  (* ---------------------------------------------------------------- *)
    24.1 --- a/src/HOLCF/IOA/meta_theory/Traces.ML	Mon Oct 17 23:10:10 2005 +0200
    24.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Mon Oct 17 23:10:13 2005 +0200
    24.3 @@ -9,7 +9,7 @@
    24.4  Delsimps (ex_simps @ all_simps);
    24.5  Delsimps [split_paired_Ex];
    24.6  Addsimps [Let_def];
    24.7 -claset_ref() := claset() delSWrapper "split_all_tac";
    24.8 +change_claset (fn cs => cs delSWrapper "split_all_tac");
    24.9  
   24.10  val exec_rws = [executions_def,is_exec_frag_def];
   24.11  
    25.1 --- a/src/HOLCF/cont_proc.ML	Mon Oct 17 23:10:10 2005 +0200
    25.2 +++ b/src/HOLCF/cont_proc.ML	Mon Oct 17 23:10:13 2005 +0200
    25.3 @@ -110,6 +110,6 @@
    25.4  end;
    25.5  
    25.6  val setup =
    25.7 -  [fn thy => Simplifier.change_simpset_of (op addsimprocs) [cont_proc thy] thy];
    25.8 +  [fn thy => (Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [cont_proc thy]); thy)];
    25.9  
   25.10  end;
    26.1 --- a/src/LCF/LCF_lemmas.ML	Mon Oct 17 23:10:10 2005 +0200
    26.2 +++ b/src/LCF/LCF_lemmas.ML	Mon Oct 17 23:10:13 2005 +0200
    26.3 @@ -92,3 +92,5 @@
    26.4           not_FF_eq_UU,not_FF_eq_TT,
    26.5           COND_UU,COND_TT,COND_FF,
    26.6           surj_pairing,FST,SND];
    26.7 +
    26.8 +change_simpset (fn _ => LCF_ss);
    27.1 --- a/src/Sequents/simpdata.ML	Mon Oct 17 23:10:10 2005 +0200
    27.2 +++ b/src/Sequents/simpdata.ML	Mon Oct 17 23:10:13 2005 +0200
    27.3 @@ -223,8 +223,6 @@
    27.4  qed "if_not_P";
    27.5  
    27.6  
    27.7 -open Simplifier;
    27.8 -
    27.9  (*** Standard simpsets ***)
   27.10  
   27.11  val triv_rls = [FalseL, TrueR, basic, refl, iff_refl, reflexive_thm];
   27.12 @@ -259,7 +257,7 @@
   27.13    addeqcongs [left_cong]
   27.14    addcongs [imp_cong];
   27.15  
   27.16 -simpset_ref() := LK_ss;
   27.17 +change_simpset (fn _ => LK_ss);
   27.18  
   27.19  
   27.20  (* To create substition rules *)
    28.1 --- a/src/ZF/Main.ML	Mon Oct 17 23:10:10 2005 +0200
    28.2 +++ b/src/ZF/Main.ML	Mon Oct 17 23:10:13 2005 +0200
    28.3 @@ -1,7 +1,7 @@
    28.4 +
    28.5 +(* $Id$ *)
    28.6  
    28.7  structure Main =
    28.8  struct
    28.9    val thy = the_context ();
   28.10  end;
   28.11 -
   28.12 -simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
    29.1 --- a/src/ZF/OrdQuant.thy	Mon Oct 17 23:10:10 2005 +0200
    29.2 +++ b/src/ZF/OrdQuant.thy	Mon Oct 17 23:10:13 2005 +0200
    29.3 @@ -392,7 +392,7 @@
    29.4      atomize ([("OrdQuant.oall", [ospec]),("OrdQuant.rall", [rspec])]@
    29.5                   ZF_conn_pairs,
    29.6               ZF_mem_pairs);
    29.7 -simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
    29.8 +change_simpset (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all));
    29.9  *}
   29.10  
   29.11  text {* Setting up the one-point-rule simproc *}
    30.1 --- a/src/ZF/simpdata.ML	Mon Oct 17 23:10:10 2005 +0200
    30.2 +++ b/src/ZF/simpdata.ML	Mon Oct 17 23:10:13 2005 +0200
    30.3 @@ -48,10 +48,10 @@
    30.4  val type_solver =
    30.5    mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems));
    30.6  
    30.7 -simpset_ref() :=
    30.8 -  simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
    30.9 +change_simpset (fn ss =>
   30.10 +  ss setmksimps (map mk_eq o ZF_atomize o gen_all)
   30.11    addcongs [if_weak_cong]
   30.12 -  setSolver type_solver;
   30.13 +  setSolver type_solver);
   30.14  
   30.15  local
   30.16