# HG changeset patch
# User wenzelm
# Date 1305323920 -7200
# Node ID 66fcc98827845cc5e76166bffaac9b9c58d3dd4c
# Parent  07155da3b2f475000e5ba05d6ed6b4bcefb832e5
clarified map_simpset versus Simplifier.map_simpset_global;

diff -r 07155da3b2f4 -r 66fcc9882784 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/FOL/FOL.thy	Fri May 13 23:58:40 2011 +0200
@@ -342,7 +342,7 @@
 val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
 *}
 
-setup {* Simplifier.map_simpset (K FOL_ss) *}
+setup {* Simplifier.map_simpset_global (K FOL_ss) *}
 
 setup "Simplifier.method_setup Splitter.split_modifiers"
 setup Splitter.setup
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/HOL.thy	Fri May 13 23:58:40 2011 +0200
@@ -1205,7 +1205,7 @@
 use "Tools/simpdata.ML"
 ML {* open Simpdata *}
 
-setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
+setup {* Simplifier.map_simpset_global (K HOL_basic_ss) *}
 
 simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
 simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Fri May 13 23:58:40 2011 +0200
@@ -83,7 +83,7 @@
 lemma last_ind_on_first:
     "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
   apply simp
-  apply (tactic {* auto_tac (map_simpset_local (fn _ =>
+  apply (tactic {* auto_tac (map_simpset (fn _ =>
     HOL_ss addsplits [@{thm list.split}]
     addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) @{context}) *})
   done
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Fri May 13 23:58:40 2011 +0200
@@ -606,7 +606,7 @@
 fun abstraction_tac ctxt =
   SELECT_GOAL (auto_tac
     (ctxt addSIs @{thms weak_strength_lemmas}
-      |> map_simpset_local (fn ss =>
+      |> map_simpset (fn ss =>
         ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}])))
 *}
 
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/HOLCF/Tools/cont_proc.ML
--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Fri May 13 23:58:40 2011 +0200
@@ -128,6 +128,6 @@
     Simplifier.simproc_global thy "cont_proc" ["cont f"] solve_cont
 end
 
-fun setup thy = Simplifier.map_simpset (fn ss => ss addsimprocs [cont_proc thy]) thy
+fun setup thy = Simplifier.map_simpset_global (fn ss => ss addsimprocs [cont_proc thy]) thy
 
 end
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Fri May 13 23:58:40 2011 +0200
@@ -1202,7 +1202,7 @@
 apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{context}]) *})
 --{* 41 subgoals left *}
 apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans},
-    force_tac (map_simpset_local (fn ss => ss addsimps
+    force_tac (map_simpset (fn ss => ss addsimps
       [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *})
 --{* 35 subgoals left *}
 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
@@ -1212,7 +1212,7 @@
 apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *})
 --{* 25 subgoals left *}
 apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans},
-    force_tac (map_simpset_local (fn ss => ss addsimps
+    force_tac (map_simpset (fn ss => ss addsimps
       [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *})
 --{* 10 subgoals left *}
 apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy	Fri May 13 23:58:40 2011 +0200
@@ -330,7 +330,7 @@
 apply(drule conforms_heapD)
 apply(tactic {*
   auto_tac (put_claset HOL_cs @{context} addEs [@{thm oconf_hext}] addDs [@{thm hconfD}]
-  |> map_simpset_local (fn ss => ss delsimps [@{thm split_paired_All}])) *})
+    |> map_simpset (fn ss => ss delsimps [@{thm split_paired_All}])) *})
 done
 
 lemma conforms_upd_local: 
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Orderings.thy	Fri May 13 23:58:40 2011 +0200
@@ -564,11 +564,12 @@
   handle THM _ => NONE;
 
 fun add_simprocs procs thy =
-  Simplifier.map_simpset (fn ss => ss
+  Simplifier.map_simpset_global (fn ss => ss
     addsimprocs (map (fn (name, raw_ts, proc) =>
       Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
+
 fun add_solver name tac =
-  Simplifier.map_simpset (fn ss => ss addSolver
+  Simplifier.map_simpset_global (fn ss => ss addSolver
     mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));
 
 in
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/TLA/TLA.thy	Fri May 13 23:58:40 2011 +0200
@@ -599,7 +599,7 @@
 *)
 fun auto_inv_tac ss =
   SELECT_GOAL
-    (inv_tac (map_simpset_local (K ss) @{context}) 1 THEN
+    (inv_tac (map_simpset (K ss) @{context}) 1 THEN
       (TRYALL (action_simp_tac
         (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
 *}
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri May 13 23:58:40 2011 +0200
@@ -216,8 +216,7 @@
 fun lexicographic_order_tac quiet ctxt =
   TRY (Function_Common.apply_termination_rule ctxt 1) THEN
   lex_order_tac quiet ctxt
-    (auto_tac
-      (map_simpset_local (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt))
+    (auto_tac (map_simpset (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt))
 
 val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac false
 
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri May 13 23:58:40 2011 +0200
@@ -338,7 +338,7 @@
 fun decomp_scnp_tac orders ctxt =
   let
     val extra_simps = Function_Common.Termination_Simps.get ctxt
-    val autom_tac = auto_tac (map_simpset_local (fn ss => ss addsimps extra_simps) ctxt)
+    val autom_tac = auto_tac (map_simpset (fn ss => ss addsimps extra_simps) ctxt)
   in
      gen_sizechange_tac orders autom_tac ctxt
   end
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Fri May 13 23:58:40 2011 +0200
@@ -557,7 +557,7 @@
   Codegen.add_preprocessor codegen_preproc #>
   Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
     "declaration of monotonicity rule for set operators" #>
-  Context.theory_map (Simplifier.map_ss (fn ss => ss addsimprocs [collect_mem_simproc]));
+  Simplifier.map_simpset_global (fn ss => ss addsimprocs [collect_mem_simproc]);
 
 
 (* outer syntax *)
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Tools/int_arith.ML	Fri May 13 23:58:40 2011 +0200
@@ -84,8 +84,8 @@
       "(m::'a::{linordered_idom,number_ring}) <= n",
       "(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
 
-val global_setup = Simplifier.map_simpset
-  (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
+val global_setup =
+  Simplifier.map_simpset_global (fn ss => ss addsimprocs [fast_int_arith_simproc]);
 
 
 fun number_of thy T n =
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Tools/recdef.ML	Fri May 13 23:58:40 2011 +0200
@@ -167,7 +167,7 @@
       | SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0));
     val {simps, congs, wfs} = get_hints ctxt;
     val ctxt' = ctxt
-      |> Context.proof_map (Simplifier.map_ss (fn ss => ss addsimps simps delcongs [imp_cong]));
+      |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]);
   in (ctxt', rev (map snd congs), wfs) end;
 
 fun prepare_hints_i thy () =
@@ -175,7 +175,7 @@
     val ctxt = Proof_Context.init_global thy;
     val {simps, congs, wfs} = get_global_hints thy;
     val ctxt' = ctxt
-      |> Context.proof_map (Simplifier.map_ss (fn ss => ss addsimps simps delcongs [imp_cong]));
+      |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]);
   in (ctxt', rev (map snd congs), wfs) end;
 
 
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Tools/record.ML	Fri May 13 23:58:40 2011 +0200
@@ -2508,8 +2508,7 @@
 val setup =
   Sign.add_trfuns ([], parse_translation, [], []) #>
   Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
-  Simplifier.map_simpset (fn ss =>
-    ss addsimprocs [simproc, upd_simproc, eq_simproc]);
+  Simplifier.map_simpset_global (fn ss => ss addsimprocs [simproc, upd_simproc, eq_simproc]);
 
 
 (* outer syntax *)
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy	Fri May 13 23:58:40 2011 +0200
@@ -1027,8 +1027,8 @@
 );
 *}
 
-declaration {* fn _ =>
-  Simplifier.map_ss (fn ss => ss
+setup {*
+  Simplifier.map_simpset_global (fn ss => ss
     addSolver (mk_solver' "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
     addSolver (mk_solver' "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
     addSolver (mk_solver' "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Fri May 13 23:58:40 2011 +0200
@@ -334,10 +334,10 @@
   let val ctxt' =
     (ctxt addIs [ext])
     |> map_claset (fn cs => cs addSWrapper Record.split_wrapper)
-    |> map_simpset_local (fn ss => ss 
-        addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
-          @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
-          @{thm o_apply}, @{thm Let_def}])
+    |> map_simpset (fn ss => ss addsimps
+       [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
+        @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
+        @{thm o_apply}, @{thm Let_def}])
   in auto_tac ctxt' end;
 
 *}
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/UNITY/UNITY_Main.thy
--- a/src/HOL/UNITY/UNITY_Main.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy	Fri May 13 23:58:40 2011 +0200
@@ -19,4 +19,10 @@
   (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
 *} "for proving progress properties"
 
+setup {*
+  Simplifier.map_simpset_global (fn ss => ss
+    addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
+    addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}))
+*}
+
 end
diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/UNITY/UNITY_tactics.ML
--- a/src/HOL/UNITY/UNITY_tactics.ML	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML	Fri May 13 23:58:40 2011 +0200
@@ -59,6 +59,3 @@
      th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
      th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];
 
-Simplifier.change_simpset (fn ss => ss
-  addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
-  addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}));
diff -r 07155da3b2f4 -r 66fcc9882784 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri May 13 23:24:06 2011 +0200
+++ b/src/Pure/simplifier.ML	Fri May 13 23:58:40 2011 +0200
@@ -8,12 +8,11 @@
 signature BASIC_SIMPLIFIER =
 sig
   include BASIC_RAW_SIMPLIFIER
-  val map_simpset_local: (simpset -> simpset) -> Proof.context -> Proof.context
-  val change_simpset: (simpset -> simpset) -> unit
+  val map_simpset: (simpset -> simpset) -> Proof.context -> Proof.context
+  val simpset_of: Proof.context -> simpset
   val global_simpset_of: theory -> simpset
   val Addsimprocs: simproc list -> unit
   val Delsimprocs: simproc list -> unit
-  val simpset_of: Proof.context -> simpset
   val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
   val safe_asm_full_simp_tac: simpset -> int -> tactic
   val simp_tac: simpset -> int -> tactic
@@ -31,6 +30,7 @@
 signature SIMPLIFIER =
 sig
   include BASIC_SIMPLIFIER
+  val map_simpset_global: (simpset -> simpset) -> theory -> theory
   val pretty_ss: Proof.context -> simpset -> Pretty.T
   val clear_ss: simpset -> simpset
   val debug_bounds: bool Unsynchronized.ref
@@ -42,10 +42,10 @@
   val context: Proof.context -> simpset -> simpset
   val global_context: theory -> simpset -> simpset
   val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
-  val simproc_global_i: theory -> string -> term list
-    -> (theory -> simpset -> term -> thm option) -> simproc
-  val simproc_global: theory -> string -> string list
-    -> (theory -> simpset -> term -> thm option) -> simproc
+  val simproc_global_i: theory -> string -> term list ->
+    (theory -> simpset -> term -> thm option) -> simproc
+  val simproc_global: theory -> string -> string list ->
+    (theory -> simpset -> term -> thm option) -> simproc
   val rewrite: simpset -> conv
   val asm_rewrite: simpset -> conv
   val full_rewrite: simpset -> conv
@@ -58,7 +58,6 @@
   val simp_del: attribute
   val cong_add: attribute
   val cong_del: attribute
-  val map_simpset: (simpset -> simpset) -> theory -> theory
   val check_simproc: Proof.context -> xstring * Position.T -> string
   val the_simproc: Proof.context -> string -> simproc
   val def_simproc: {name: binding, lhss: term list,
@@ -135,26 +134,25 @@
 val cong_del = attrib (op delcongs);
 
 
-(* global simpset *)
-
-fun map_simpset f = Context.theory_map (map_ss f);  (* FIXME global *)
-fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
-fun global_simpset_of thy =
-  Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy));
-
-fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
-fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
-
-
 (* local simpset *)
 
-fun map_simpset_local f = Context.proof_map (map_ss f);
+fun map_simpset f = Context.proof_map (map_ss f);
 fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt));
 
 val _ = ML_Antiquote.value "simpset"
   (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())");
 
 
+(* global simpset *)
+
+fun map_simpset_global f = Context.theory_map (map_ss f);
+fun global_simpset_of thy =
+  Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy));
+
+fun Addsimprocs args = Context.>> (map_ss (fn ss => ss addsimprocs args));
+fun Delsimprocs args = Context.>> (map_ss (fn ss => ss delsimprocs args));
+
+
 
 (** named simprocs **)
 
diff -r 07155da3b2f4 -r 66fcc9882784 src/Sequents/LK.thy
--- a/src/Sequents/LK.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/Sequents/LK.thy	Fri May 13 23:58:40 2011 +0200
@@ -216,6 +216,7 @@
   done
 
 use "simpdata.ML"
+setup {* Simplifier.map_simpset_global (K LK_ss) *}
 
 
 text {* To create substition rules *}
diff -r 07155da3b2f4 -r 66fcc9882784 src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Fri May 13 23:24:06 2011 +0200
+++ b/src/Sequents/simpdata.ML	Fri May 13 23:58:40 2011 +0200
@@ -88,4 +88,3 @@
   addeqcongs [@{thm left_cong}]
   addcongs [@{thm imp_cong}];
 
-change_simpset (fn _ => LK_ss);
diff -r 07155da3b2f4 -r 66fcc9882784 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Fri May 13 23:24:06 2011 +0200
+++ b/src/ZF/Tools/typechk.ML	Fri May 13 23:58:40 2011 +0200
@@ -130,6 +130,6 @@
 val setup =
   Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
   typecheck_setup #>
-  Simplifier.map_simpset (fn ss => ss setSolver type_solver);
+  Simplifier.map_simpset_global (fn ss => ss setSolver type_solver);
 
 end;
diff -r 07155da3b2f4 -r 66fcc9882784 src/ZF/pair.thy
--- a/src/ZF/pair.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/ZF/pair.thy	Fri May 13 23:58:40 2011 +0200
@@ -9,8 +9,8 @@
 uses "simpdata.ML"
 begin
 
-declaration {*
-  fn _ => Simplifier.map_ss (fn ss =>
+setup {*
+  Simplifier.map_simpset_global (fn ss =>
     ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
     addcongs [@{thm if_weak_cong}])
 *}