clarified map_simpset versus Simplifier.map_simpset_global;
authorwenzelm
Fri May 13 23:58:40 2011 +0200 (2011-05-13)
changeset 4279566fcc9882784
parent 42794 07155da3b2f4
child 42797 f092945f0ef7
clarified map_simpset versus Simplifier.map_simpset_global;
src/FOL/FOL.thy
src/HOL/HOL.thy
src/HOL/HOLCF/IOA/ABP/Correctness.thy
src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOL/HOLCF/Tools/cont_proc.ML
src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
src/HOL/MicroJava/J/Conform.thy
src/HOL/Orderings.thy
src/HOL/TLA/TLA.thy
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/record.ML
src/HOL/Transitive_Closure.thy
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/UNITY_Main.thy
src/HOL/UNITY/UNITY_tactics.ML
src/Pure/simplifier.ML
src/Sequents/LK.thy
src/Sequents/simpdata.ML
src/ZF/Tools/typechk.ML
src/ZF/pair.thy
     1.1 --- a/src/FOL/FOL.thy	Fri May 13 23:24:06 2011 +0200
     1.2 +++ b/src/FOL/FOL.thy	Fri May 13 23:58:40 2011 +0200
     1.3 @@ -342,7 +342,7 @@
     1.4  val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
     1.5  *}
     1.6  
     1.7 -setup {* Simplifier.map_simpset (K FOL_ss) *}
     1.8 +setup {* Simplifier.map_simpset_global (K FOL_ss) *}
     1.9  
    1.10  setup "Simplifier.method_setup Splitter.split_modifiers"
    1.11  setup Splitter.setup
     2.1 --- a/src/HOL/HOL.thy	Fri May 13 23:24:06 2011 +0200
     2.2 +++ b/src/HOL/HOL.thy	Fri May 13 23:58:40 2011 +0200
     2.3 @@ -1205,7 +1205,7 @@
     2.4  use "Tools/simpdata.ML"
     2.5  ML {* open Simpdata *}
     2.6  
     2.7 -setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
     2.8 +setup {* Simplifier.map_simpset_global (K HOL_basic_ss) *}
     2.9  
    2.10  simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
    2.11  simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}
     3.1 --- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Fri May 13 23:24:06 2011 +0200
     3.2 +++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Fri May 13 23:58:40 2011 +0200
     3.3 @@ -83,7 +83,7 @@
     3.4  lemma last_ind_on_first:
     3.5      "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
     3.6    apply simp
     3.7 -  apply (tactic {* auto_tac (map_simpset_local (fn _ =>
     3.8 +  apply (tactic {* auto_tac (map_simpset (fn _ =>
     3.9      HOL_ss addsplits [@{thm list.split}]
    3.10      addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) @{context}) *})
    3.11    done
     4.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Fri May 13 23:24:06 2011 +0200
     4.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Fri May 13 23:58:40 2011 +0200
     4.3 @@ -606,7 +606,7 @@
     4.4  fun abstraction_tac ctxt =
     4.5    SELECT_GOAL (auto_tac
     4.6      (ctxt addSIs @{thms weak_strength_lemmas}
     4.7 -      |> map_simpset_local (fn ss =>
     4.8 +      |> map_simpset (fn ss =>
     4.9          ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}])))
    4.10  *}
    4.11  
     5.1 --- a/src/HOL/HOLCF/Tools/cont_proc.ML	Fri May 13 23:24:06 2011 +0200
     5.2 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Fri May 13 23:58:40 2011 +0200
     5.3 @@ -128,6 +128,6 @@
     5.4      Simplifier.simproc_global thy "cont_proc" ["cont f"] solve_cont
     5.5  end
     5.6  
     5.7 -fun setup thy = Simplifier.map_simpset (fn ss => ss addsimprocs [cont_proc thy]) thy
     5.8 +fun setup thy = Simplifier.map_simpset_global (fn ss => ss addsimprocs [cont_proc thy]) thy
     5.9  
    5.10  end
     6.1 --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Fri May 13 23:24:06 2011 +0200
     6.2 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Fri May 13 23:58:40 2011 +0200
     6.3 @@ -1202,7 +1202,7 @@
     6.4  apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{context}]) *})
     6.5  --{* 41 subgoals left *}
     6.6  apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans},
     6.7 -    force_tac (map_simpset_local (fn ss => ss addsimps
     6.8 +    force_tac (map_simpset (fn ss => ss addsimps
     6.9        [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *})
    6.10  --{* 35 subgoals left *}
    6.11  apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
    6.12 @@ -1212,7 +1212,7 @@
    6.13  apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *})
    6.14  --{* 25 subgoals left *}
    6.15  apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans},
    6.16 -    force_tac (map_simpset_local (fn ss => ss addsimps
    6.17 +    force_tac (map_simpset (fn ss => ss addsimps
    6.18        [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *})
    6.19  --{* 10 subgoals left *}
    6.20  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)+
     7.1 --- a/src/HOL/MicroJava/J/Conform.thy	Fri May 13 23:24:06 2011 +0200
     7.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Fri May 13 23:58:40 2011 +0200
     7.3 @@ -330,7 +330,7 @@
     7.4  apply(drule conforms_heapD)
     7.5  apply(tactic {*
     7.6    auto_tac (put_claset HOL_cs @{context} addEs [@{thm oconf_hext}] addDs [@{thm hconfD}]
     7.7 -  |> map_simpset_local (fn ss => ss delsimps [@{thm split_paired_All}])) *})
     7.8 +    |> map_simpset (fn ss => ss delsimps [@{thm split_paired_All}])) *})
     7.9  done
    7.10  
    7.11  lemma conforms_upd_local: 
     8.1 --- a/src/HOL/Orderings.thy	Fri May 13 23:24:06 2011 +0200
     8.2 +++ b/src/HOL/Orderings.thy	Fri May 13 23:58:40 2011 +0200
     8.3 @@ -564,11 +564,12 @@
     8.4    handle THM _ => NONE;
     8.5  
     8.6  fun add_simprocs procs thy =
     8.7 -  Simplifier.map_simpset (fn ss => ss
     8.8 +  Simplifier.map_simpset_global (fn ss => ss
     8.9      addsimprocs (map (fn (name, raw_ts, proc) =>
    8.10        Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
    8.11 +
    8.12  fun add_solver name tac =
    8.13 -  Simplifier.map_simpset (fn ss => ss addSolver
    8.14 +  Simplifier.map_simpset_global (fn ss => ss addSolver
    8.15      mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));
    8.16  
    8.17  in
     9.1 --- a/src/HOL/TLA/TLA.thy	Fri May 13 23:24:06 2011 +0200
     9.2 +++ b/src/HOL/TLA/TLA.thy	Fri May 13 23:58:40 2011 +0200
     9.3 @@ -599,7 +599,7 @@
     9.4  *)
     9.5  fun auto_inv_tac ss =
     9.6    SELECT_GOAL
     9.7 -    (inv_tac (map_simpset_local (K ss) @{context}) 1 THEN
     9.8 +    (inv_tac (map_simpset (K ss) @{context}) 1 THEN
     9.9        (TRYALL (action_simp_tac
    9.10          (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
    9.11  *}
    10.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri May 13 23:24:06 2011 +0200
    10.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri May 13 23:58:40 2011 +0200
    10.3 @@ -216,8 +216,7 @@
    10.4  fun lexicographic_order_tac quiet ctxt =
    10.5    TRY (Function_Common.apply_termination_rule ctxt 1) THEN
    10.6    lex_order_tac quiet ctxt
    10.7 -    (auto_tac
    10.8 -      (map_simpset_local (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt))
    10.9 +    (auto_tac (map_simpset (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt))
   10.10  
   10.11  val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac false
   10.12  
    11.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri May 13 23:24:06 2011 +0200
    11.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri May 13 23:58:40 2011 +0200
    11.3 @@ -338,7 +338,7 @@
    11.4  fun decomp_scnp_tac orders ctxt =
    11.5    let
    11.6      val extra_simps = Function_Common.Termination_Simps.get ctxt
    11.7 -    val autom_tac = auto_tac (map_simpset_local (fn ss => ss addsimps extra_simps) ctxt)
    11.8 +    val autom_tac = auto_tac (map_simpset (fn ss => ss addsimps extra_simps) ctxt)
    11.9    in
   11.10       gen_sizechange_tac orders autom_tac ctxt
   11.11    end
    12.1 --- a/src/HOL/Tools/inductive_set.ML	Fri May 13 23:24:06 2011 +0200
    12.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri May 13 23:58:40 2011 +0200
    12.3 @@ -557,7 +557,7 @@
    12.4    Codegen.add_preprocessor codegen_preproc #>
    12.5    Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
    12.6      "declaration of monotonicity rule for set operators" #>
    12.7 -  Context.theory_map (Simplifier.map_ss (fn ss => ss addsimprocs [collect_mem_simproc]));
    12.8 +  Simplifier.map_simpset_global (fn ss => ss addsimprocs [collect_mem_simproc]);
    12.9  
   12.10  
   12.11  (* outer syntax *)
    13.1 --- a/src/HOL/Tools/int_arith.ML	Fri May 13 23:24:06 2011 +0200
    13.2 +++ b/src/HOL/Tools/int_arith.ML	Fri May 13 23:58:40 2011 +0200
    13.3 @@ -84,8 +84,8 @@
    13.4        "(m::'a::{linordered_idom,number_ring}) <= n",
    13.5        "(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
    13.6  
    13.7 -val global_setup = Simplifier.map_simpset
    13.8 -  (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
    13.9 +val global_setup =
   13.10 +  Simplifier.map_simpset_global (fn ss => ss addsimprocs [fast_int_arith_simproc]);
   13.11  
   13.12  
   13.13  fun number_of thy T n =
    14.1 --- a/src/HOL/Tools/recdef.ML	Fri May 13 23:24:06 2011 +0200
    14.2 +++ b/src/HOL/Tools/recdef.ML	Fri May 13 23:58:40 2011 +0200
    14.3 @@ -167,7 +167,7 @@
    14.4        | SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0));
    14.5      val {simps, congs, wfs} = get_hints ctxt;
    14.6      val ctxt' = ctxt
    14.7 -      |> Context.proof_map (Simplifier.map_ss (fn ss => ss addsimps simps delcongs [imp_cong]));
    14.8 +      |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]);
    14.9    in (ctxt', rev (map snd congs), wfs) end;
   14.10  
   14.11  fun prepare_hints_i thy () =
   14.12 @@ -175,7 +175,7 @@
   14.13      val ctxt = Proof_Context.init_global thy;
   14.14      val {simps, congs, wfs} = get_global_hints thy;
   14.15      val ctxt' = ctxt
   14.16 -      |> Context.proof_map (Simplifier.map_ss (fn ss => ss addsimps simps delcongs [imp_cong]));
   14.17 +      |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]);
   14.18    in (ctxt', rev (map snd congs), wfs) end;
   14.19  
   14.20  
    15.1 --- a/src/HOL/Tools/record.ML	Fri May 13 23:24:06 2011 +0200
    15.2 +++ b/src/HOL/Tools/record.ML	Fri May 13 23:58:40 2011 +0200
    15.3 @@ -2508,8 +2508,7 @@
    15.4  val setup =
    15.5    Sign.add_trfuns ([], parse_translation, [], []) #>
    15.6    Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
    15.7 -  Simplifier.map_simpset (fn ss =>
    15.8 -    ss addsimprocs [simproc, upd_simproc, eq_simproc]);
    15.9 +  Simplifier.map_simpset_global (fn ss => ss addsimprocs [simproc, upd_simproc, eq_simproc]);
   15.10  
   15.11  
   15.12  (* outer syntax *)
    16.1 --- a/src/HOL/Transitive_Closure.thy	Fri May 13 23:24:06 2011 +0200
    16.2 +++ b/src/HOL/Transitive_Closure.thy	Fri May 13 23:58:40 2011 +0200
    16.3 @@ -1027,8 +1027,8 @@
    16.4  );
    16.5  *}
    16.6  
    16.7 -declaration {* fn _ =>
    16.8 -  Simplifier.map_ss (fn ss => ss
    16.9 +setup {*
   16.10 +  Simplifier.map_simpset_global (fn ss => ss
   16.11      addSolver (mk_solver' "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
   16.12      addSolver (mk_solver' "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
   16.13      addSolver (mk_solver' "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))
    17.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Fri May 13 23:24:06 2011 +0200
    17.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Fri May 13 23:58:40 2011 +0200
    17.3 @@ -334,10 +334,10 @@
    17.4    let val ctxt' =
    17.5      (ctxt addIs [ext])
    17.6      |> map_claset (fn cs => cs addSWrapper Record.split_wrapper)
    17.7 -    |> map_simpset_local (fn ss => ss 
    17.8 -        addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
    17.9 -          @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
   17.10 -          @{thm o_apply}, @{thm Let_def}])
   17.11 +    |> map_simpset (fn ss => ss addsimps
   17.12 +       [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
   17.13 +        @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
   17.14 +        @{thm o_apply}, @{thm Let_def}])
   17.15    in auto_tac ctxt' end;
   17.16  
   17.17  *}
    18.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Fri May 13 23:24:06 2011 +0200
    18.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Fri May 13 23:58:40 2011 +0200
    18.3 @@ -19,4 +19,10 @@
    18.4    (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
    18.5  *} "for proving progress properties"
    18.6  
    18.7 +setup {*
    18.8 +  Simplifier.map_simpset_global (fn ss => ss
    18.9 +    addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
   18.10 +    addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}))
   18.11 +*}
   18.12 +
   18.13  end
    19.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Fri May 13 23:24:06 2011 +0200
    19.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Fri May 13 23:58:40 2011 +0200
    19.3 @@ -59,6 +59,3 @@
    19.4       th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
    19.5       th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];
    19.6  
    19.7 -Simplifier.change_simpset (fn ss => ss
    19.8 -  addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
    19.9 -  addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}));
    20.1 --- a/src/Pure/simplifier.ML	Fri May 13 23:24:06 2011 +0200
    20.2 +++ b/src/Pure/simplifier.ML	Fri May 13 23:58:40 2011 +0200
    20.3 @@ -8,12 +8,11 @@
    20.4  signature BASIC_SIMPLIFIER =
    20.5  sig
    20.6    include BASIC_RAW_SIMPLIFIER
    20.7 -  val map_simpset_local: (simpset -> simpset) -> Proof.context -> Proof.context
    20.8 -  val change_simpset: (simpset -> simpset) -> unit
    20.9 +  val map_simpset: (simpset -> simpset) -> Proof.context -> Proof.context
   20.10 +  val simpset_of: Proof.context -> simpset
   20.11    val global_simpset_of: theory -> simpset
   20.12    val Addsimprocs: simproc list -> unit
   20.13    val Delsimprocs: simproc list -> unit
   20.14 -  val simpset_of: Proof.context -> simpset
   20.15    val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
   20.16    val safe_asm_full_simp_tac: simpset -> int -> tactic
   20.17    val simp_tac: simpset -> int -> tactic
   20.18 @@ -31,6 +30,7 @@
   20.19  signature SIMPLIFIER =
   20.20  sig
   20.21    include BASIC_SIMPLIFIER
   20.22 +  val map_simpset_global: (simpset -> simpset) -> theory -> theory
   20.23    val pretty_ss: Proof.context -> simpset -> Pretty.T
   20.24    val clear_ss: simpset -> simpset
   20.25    val debug_bounds: bool Unsynchronized.ref
   20.26 @@ -42,10 +42,10 @@
   20.27    val context: Proof.context -> simpset -> simpset
   20.28    val global_context: theory -> simpset -> simpset
   20.29    val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
   20.30 -  val simproc_global_i: theory -> string -> term list
   20.31 -    -> (theory -> simpset -> term -> thm option) -> simproc
   20.32 -  val simproc_global: theory -> string -> string list
   20.33 -    -> (theory -> simpset -> term -> thm option) -> simproc
   20.34 +  val simproc_global_i: theory -> string -> term list ->
   20.35 +    (theory -> simpset -> term -> thm option) -> simproc
   20.36 +  val simproc_global: theory -> string -> string list ->
   20.37 +    (theory -> simpset -> term -> thm option) -> simproc
   20.38    val rewrite: simpset -> conv
   20.39    val asm_rewrite: simpset -> conv
   20.40    val full_rewrite: simpset -> conv
   20.41 @@ -58,7 +58,6 @@
   20.42    val simp_del: attribute
   20.43    val cong_add: attribute
   20.44    val cong_del: attribute
   20.45 -  val map_simpset: (simpset -> simpset) -> theory -> theory
   20.46    val check_simproc: Proof.context -> xstring * Position.T -> string
   20.47    val the_simproc: Proof.context -> string -> simproc
   20.48    val def_simproc: {name: binding, lhss: term list,
   20.49 @@ -135,26 +134,25 @@
   20.50  val cong_del = attrib (op delcongs);
   20.51  
   20.52  
   20.53 -(* global simpset *)
   20.54 -
   20.55 -fun map_simpset f = Context.theory_map (map_ss f);  (* FIXME global *)
   20.56 -fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
   20.57 -fun global_simpset_of thy =
   20.58 -  Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy));
   20.59 -
   20.60 -fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
   20.61 -fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
   20.62 -
   20.63 -
   20.64  (* local simpset *)
   20.65  
   20.66 -fun map_simpset_local f = Context.proof_map (map_ss f);
   20.67 +fun map_simpset f = Context.proof_map (map_ss f);
   20.68  fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt));
   20.69  
   20.70  val _ = ML_Antiquote.value "simpset"
   20.71    (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())");
   20.72  
   20.73  
   20.74 +(* global simpset *)
   20.75 +
   20.76 +fun map_simpset_global f = Context.theory_map (map_ss f);
   20.77 +fun global_simpset_of thy =
   20.78 +  Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy));
   20.79 +
   20.80 +fun Addsimprocs args = Context.>> (map_ss (fn ss => ss addsimprocs args));
   20.81 +fun Delsimprocs args = Context.>> (map_ss (fn ss => ss delsimprocs args));
   20.82 +
   20.83 +
   20.84  
   20.85  (** named simprocs **)
   20.86  
    21.1 --- a/src/Sequents/LK.thy	Fri May 13 23:24:06 2011 +0200
    21.2 +++ b/src/Sequents/LK.thy	Fri May 13 23:58:40 2011 +0200
    21.3 @@ -216,6 +216,7 @@
    21.4    done
    21.5  
    21.6  use "simpdata.ML"
    21.7 +setup {* Simplifier.map_simpset_global (K LK_ss) *}
    21.8  
    21.9  
   21.10  text {* To create substition rules *}
    22.1 --- a/src/Sequents/simpdata.ML	Fri May 13 23:24:06 2011 +0200
    22.2 +++ b/src/Sequents/simpdata.ML	Fri May 13 23:58:40 2011 +0200
    22.3 @@ -88,4 +88,3 @@
    22.4    addeqcongs [@{thm left_cong}]
    22.5    addcongs [@{thm imp_cong}];
    22.6  
    22.7 -change_simpset (fn _ => LK_ss);
    23.1 --- a/src/ZF/Tools/typechk.ML	Fri May 13 23:24:06 2011 +0200
    23.2 +++ b/src/ZF/Tools/typechk.ML	Fri May 13 23:58:40 2011 +0200
    23.3 @@ -130,6 +130,6 @@
    23.4  val setup =
    23.5    Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
    23.6    typecheck_setup #>
    23.7 -  Simplifier.map_simpset (fn ss => ss setSolver type_solver);
    23.8 +  Simplifier.map_simpset_global (fn ss => ss setSolver type_solver);
    23.9  
   23.10  end;
    24.1 --- a/src/ZF/pair.thy	Fri May 13 23:24:06 2011 +0200
    24.2 +++ b/src/ZF/pair.thy	Fri May 13 23:58:40 2011 +0200
    24.3 @@ -9,8 +9,8 @@
    24.4  uses "simpdata.ML"
    24.5  begin
    24.6  
    24.7 -declaration {*
    24.8 -  fn _ => Simplifier.map_ss (fn ss =>
    24.9 +setup {*
   24.10 +  Simplifier.map_simpset_global (fn ss =>
   24.11      ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
   24.12      addcongs [@{thm if_weak_cong}])
   24.13  *}