# HG changeset patch
# User wenzelm
# Date 1205963255 -3600
# Node ID 7825c83c9efff5d358abea0c57fa46b408c2c348
# Parent  f8ed02f224335dc00070d028875fd390ea3e1755
eliminated change_claset/simpset;

diff -r f8ed02f22433 -r 7825c83c9eff src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Wed Mar 19 22:28:17 2008 +0100
+++ b/src/HOL/Datatype.thy	Wed Mar 19 22:47:35 2008 +0100
@@ -635,7 +635,9 @@
 lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
   by simp
 
-ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *}
+declaration {* fn _ =>
+  Classical.map_cs (fn cs => cs addSD2 ("ospec", thm "ospec"))
+*}
 
 lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
   by (cases xo) auto
diff -r f8ed02f22433 -r 7825c83c9eff src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Mar 19 22:28:17 2008 +0100
+++ b/src/HOL/Set.thy	Wed Mar 19 22:47:35 2008 +0100
@@ -428,8 +428,8 @@
   Gives better instantiation for bound:
 *}
 
-ML_setup {*
-  change_claset (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
+declaration {* fn _ =>
+  Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
 *}
 
 lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
@@ -1031,9 +1031,11 @@
    ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
  *)
 
-ML_setup {*
+ML {*
   val mksimps_pairs = [("Ball", @{thms bspec})] @ mksimps_pairs;
-  change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
+*}
+declaration {* fn _ =>
+  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
 *}
 
 
diff -r f8ed02f22433 -r 7825c83c9eff src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Wed Mar 19 22:28:17 2008 +0100
+++ b/src/HOLCF/HOLCF.thy	Wed Mar 19 22:47:35 2008 +0100
@@ -21,8 +21,8 @@
 
 defaultsort pcpo
 
-ML_setup {*
-  change_simpset (fn simpset => simpset addSolver
+declaration {* fn _ =>
+  Simplifier.map_ss (fn simpset => simpset addSolver
     (mk_solver' "adm_tac" (fn ss =>
       adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
 *}
diff -r f8ed02f22433 -r 7825c83c9eff src/HOLCF/IOA/NTP/Correctness.thy
--- a/src/HOLCF/IOA/NTP/Correctness.thy	Wed Mar 19 22:28:17 2008 +0100
+++ b/src/HOLCF/IOA/NTP/Correctness.thy	Wed Mar 19 22:47:35 2008 +0100
@@ -14,9 +14,9 @@
   "hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
                          else tl(sq(sen s)))"
 
-ML_setup {*
-(* repeated from Traces.ML *)
-change_claset (fn cs => cs delSWrapper "split_all_tac")
+declaration {* fn _ =>
+  (* repeated from Traces.ML *)
+  Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")
 *}
 
 lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas
diff -r f8ed02f22433 -r 7825c83c9eff src/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Mar 19 22:28:17 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Mar 19 22:47:35 2008 +0100
@@ -68,7 +68,7 @@
   "Finite (mksch A B$tr$x$y) --> Finite tr"
 
 
-ML_setup {* change_simpset (fn ss => ss setmksym (K NONE)) *}
+declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K NONE)) *}
 
 
 subsection "mksch rewrite rules"
@@ -967,7 +967,7 @@
 done
 
 
-ML_setup {* change_simpset (fn ss => ss setmksym (SOME o symmetric_fun)) *}
+declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (SOME o symmetric_fun)) *}
 
 
 end
diff -r f8ed02f22433 -r 7825c83c9eff src/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Mar 19 22:28:17 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Mar 19 22:47:35 2008 +0100
@@ -90,7 +90,7 @@
 lemmas [simp del] = ex_simps all_simps split_paired_Ex
 declare Let_def [simp]
 
-ML_setup {* change_claset (fn cs => cs delSWrapper "split_all_tac") *}
+declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
 
 
 subsection {* ex2seqC *}
diff -r f8ed02f22433 -r 7825c83c9eff src/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOLCF/IOA/meta_theory/Traces.thy	Wed Mar 19 22:28:17 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Wed Mar 19 22:47:35 2008 +0100
@@ -195,7 +195,7 @@
 
 lemmas [simp del] = ex_simps all_simps split_paired_Ex
 declare Let_def [simp]
-ML_setup {* change_claset (fn cs => cs delSWrapper "split_all_tac") *}
+declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
 
 lemmas exec_rws = executions_def is_exec_frag_def
 
diff -r f8ed02f22433 -r 7825c83c9eff src/ZF/Main_ZF.thy
--- a/src/ZF/Main_ZF.thy	Wed Mar 19 22:28:17 2008 +0100
+++ b/src/ZF/Main_ZF.thy	Wed Mar 19 22:47:35 2008 +0100
@@ -72,8 +72,8 @@
 by (rule transrec3_def [THEN def_transrec, THEN trans], force)
 
 
-ML_setup {*
-  change_simpset (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all));
+declaration {* fn _ =>
+  Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
 *}
 
 end
diff -r f8ed02f22433 -r 7825c83c9eff src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Wed Mar 19 22:28:17 2008 +0100
+++ b/src/ZF/OrdQuant.thy	Wed Mar 19 22:47:35 2008 +0100
@@ -362,7 +362,9 @@
     atomize ([("OrdQuant.oall", [@{thm ospec}]),("OrdQuant.rall", [@{thm rspec}])]@
                  ZF_conn_pairs,
              ZF_mem_pairs);
-change_simpset (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all));
+*}
+declaration {* fn _ =>
+  Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
 *}
 
 text {* Setting up the one-point-rule simproc *}