modernized some old-style infix operations, which were left over from the time of ML proof scripts;
authorwenzelm
Thu Nov 24 21:01:06 2011 +0100 (2011-11-24)
changeset 45625750c5a47400b
parent 45624 329bc52b4b86
child 45626 b4f374a45668
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
NEWS
src/FOL/simpdata.ML
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/ringsimp.ML
src/HOL/HOL.thy
src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Prolog/prolog.ML
src/HOL/Set.thy
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/abel_cancel.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/simpdata.ML
src/Provers/hypsubst.ML
src/Pure/raw_simplifier.ML
src/Pure/simplifier.ML
src/Sequents/simpdata.ML
src/ZF/Main_ZF.thy
src/ZF/OrdQuant.thy
src/ZF/Tools/inductive_package.ML
src/ZF/pair.thy
     1.1 --- a/NEWS	Thu Nov 24 20:45:34 2011 +0100
     1.2 +++ b/NEWS	Thu Nov 24 21:01:06 2011 +0100
     1.3 @@ -173,6 +173,12 @@
     1.4    deleqcongs    ~> Simplifier.del_eqcong
     1.5    addcongs      ~> Simplifier.add_cong
     1.6    delcongs      ~> Simplifier.del_cong
     1.7 +  setmksimps    ~> Simplifier.set_mksimps
     1.8 +  setmkcong     ~> Simplifier.set_mkcong
     1.9 +  setmksym      ~> Simplifier.set_mksym
    1.10 +  setmkeqTrue   ~> Simplifier.set_mkeqTrue
    1.11 +  settermless   ~> Simplifier.set_termless
    1.12 +  setsubgoaler  ~> Simplifier.set_subgoaler
    1.13    addsplits     ~> Splitter.add_split
    1.14    delsplits     ~> Splitter.del_split
    1.15  
     2.1 --- a/src/FOL/simpdata.ML	Thu Nov 24 20:45:34 2011 +0100
     2.2 +++ b/src/FOL/simpdata.ML	Thu Nov 24 21:01:06 2011 +0100
     2.3 @@ -116,11 +116,11 @@
     2.4  (*No simprules, but basic infastructure for simplification*)
     2.5  val FOL_basic_ss =
     2.6    Simplifier.global_context @{theory} empty_ss
     2.7 -  setsubgoaler asm_simp_tac
     2.8    setSSolver (mk_solver "FOL safe" safe_solver)
     2.9    setSolver (mk_solver "FOL unsafe" unsafe_solver)
    2.10 -  setmksimps (mksimps mksimps_pairs)
    2.11 -  setmkcong mk_meta_cong;
    2.12 +  |> Simplifier.set_subgoaler asm_simp_tac
    2.13 +  |> Simplifier.set_mksimps (mksimps mksimps_pairs)
    2.14 +  |> Simplifier.set_mkcong mk_meta_cong;
    2.15  
    2.16  fun unfold_tac ths =
    2.17    let val ss0 = Simplifier.clear_ss FOL_basic_ss addsimps ths
     3.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Thu Nov 24 20:45:34 2011 +0100
     3.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Thu Nov 24 21:01:06 2011 +0100
     3.3 @@ -210,7 +210,9 @@
     3.4  
     3.5  fun termless_ring (a, b) = (Term_Ord.term_lpo ring_ord (a, b) = LESS);
     3.6  
     3.7 -val ring_ss = HOL_basic_ss settermless termless_ring addsimps
     3.8 +val ring_ss =
     3.9 +  (HOL_basic_ss |> Simplifier.set_termless termless_ring)
    3.10 +  addsimps
    3.11    [@{thm a_assoc}, @{thm l_zero}, @{thm l_neg}, @{thm a_comm}, @{thm m_assoc},
    3.12     @{thm l_one}, @{thm l_distr}, @{thm m_comm}, @{thm minus_def},
    3.13     @{thm r_zero}, @{thm r_neg}, @{thm r_neg2}, @{thm r_neg1}, @{thm minus_add},
     4.1 --- a/src/HOL/Algebra/ringsimp.ML	Thu Nov 24 20:45:34 2011 +0100
     4.2 +++ b/src/HOL/Algebra/ringsimp.ML	Thu Nov 24 21:01:06 2011 +0100
     4.3 @@ -47,7 +47,7 @@
     4.4      fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops
     4.5        | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops;
     4.6      fun less (a, b) = (Term_Ord.term_lpo ord (a, b) = LESS);
     4.7 -  in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
     4.8 +  in asm_full_simp_tac (HOL_ss addsimps simps |> Simplifier.set_termless less) end;
     4.9  
    4.10  fun algebra_tac ctxt =
    4.11    EVERY' (map (fn s => TRY o struct_tac s) (Data.get (Context.Proof ctxt)));
     5.1 --- a/src/HOL/HOL.thy	Thu Nov 24 20:45:34 2011 +0100
     5.2 +++ b/src/HOL/HOL.thy	Thu Nov 24 21:01:06 2011 +0100
     5.3 @@ -1495,9 +1495,6 @@
     5.4  setup {*
     5.5    Induct.setup #> Induction.setup #>
     5.6    Context.theory_map (Induct.map_simpset (fn ss => ss
     5.7 -    setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
     5.8 -      map (Simplifier.rewrite_rule (map Thm.symmetric
     5.9 -        @{thms induct_rulify_fallback})))
    5.10      addsimprocs
    5.11        [Simplifier.simproc_global @{theory} "swap_induct_false"
    5.12           ["induct_false ==> PROP P ==> PROP Q"]
    5.13 @@ -1517,7 +1514,10 @@
    5.14                      | is_conj @{const induct_false} = true
    5.15                      | is_conj _ = false
    5.16                  in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
    5.17 -              | _ => NONE))]))
    5.18 +              | _ => NONE))]
    5.19 +    |> Simplifier.set_mksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
    5.20 +      map (Simplifier.rewrite_rule (map Thm.symmetric
    5.21 +        @{thms induct_rulify_fallback})))))
    5.22  *}
    5.23  
    5.24  text {* Pre-simplification of induction and cases rules *}
     6.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Nov 24 20:45:34 2011 +0100
     6.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Nov 24 21:01:06 2011 +0100
     6.3 @@ -67,7 +67,7 @@
     6.4    "Finite (mksch A B$tr$x$y) --> Finite tr"
     6.5  
     6.6  
     6.7 -declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K (K NONE))) *}
     6.8 +declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (K NONE))) *}
     6.9  
    6.10  
    6.11  subsection "mksch rewrite rules"
    6.12 @@ -967,7 +967,7 @@
    6.13  done
    6.14  
    6.15  
    6.16 -declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K (SOME o symmetric_fun))) *}
    6.17 +declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (SOME o symmetric_fun))) *}
    6.18  
    6.19  
    6.20  end
     7.1 --- a/src/HOL/Nominal/Nominal.thy	Thu Nov 24 20:45:34 2011 +0100
     7.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Nov 24 21:01:06 2011 +0100
     7.3 @@ -378,7 +378,7 @@
     7.4    val mksimps_pairs = (@{const_name Nominal.fresh}, @{thms fresh_prodD}) :: mksimps_pairs;
     7.5  *}
     7.6  declaration {* fn _ =>
     7.7 -  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
     7.8 +  Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs))
     7.9  *}
    7.10  
    7.11  section {* Abstract Properties for Permutations and  Atoms *}
     8.1 --- a/src/HOL/Prolog/prolog.ML	Thu Nov 24 20:45:34 2011 +0100
     8.2 +++ b/src/HOL/Prolog/prolog.ML	Thu Nov 24 21:01:06 2011 +0100
     8.3 @@ -59,14 +59,15 @@
     8.4  in map zero_var_indexes (at thm) end;
     8.5  
     8.6  val atomize_ss =
     8.7 -  Simplifier.global_context @{theory} empty_ss
     8.8 -  setmksimps (mksimps mksimps_pairs)
     8.9 +  (Simplifier.global_context @{theory} empty_ss
    8.10 +    |> Simplifier.set_mksimps (mksimps mksimps_pairs))
    8.11    addsimps [
    8.12          all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
    8.13          imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
    8.14          imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
    8.15          imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
    8.16  
    8.17 +
    8.18  (*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>
    8.19                                    resolve_tac (maps atomizeD prems) 1);
    8.20    -- is nice, but cannot instantiate unknowns in the assumptions *)
     9.1 --- a/src/HOL/Set.thy	Thu Nov 24 20:45:34 2011 +0100
     9.2 +++ b/src/HOL/Set.thy	Thu Nov 24 21:01:06 2011 +0100
     9.3 @@ -369,7 +369,7 @@
     9.4  *}
     9.5  
     9.6  declaration {* fn _ =>
     9.7 -  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
     9.8 +  Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs))
     9.9  *}
    9.10  
    9.11  lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
    10.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Nov 24 20:45:34 2011 +0100
    10.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Nov 24 21:01:06 2011 +0100
    10.3 @@ -31,8 +31,8 @@
    10.4  (* need to set up our own minimal simpset.    *)
    10.5  fun mk_minimal_ss ctxt =
    10.6    Simplifier.context ctxt empty_ss
    10.7 -    setsubgoaler asm_simp_tac
    10.8 -    setmksimps (mksimps [])
    10.9 +  |> Simplifier.set_subgoaler asm_simp_tac
   10.10 +  |> Simplifier.set_mksimps (mksimps [])
   10.11  
   10.12  (* composition of two theorems, used in maps *)
   10.13  fun OF1 thm1 thm2 = thm2 RS thm1
    11.1 --- a/src/HOL/Tools/abel_cancel.ML	Thu Nov 24 20:45:34 2011 +0100
    11.2 +++ b/src/HOL/Tools/abel_cancel.ML	Thu Nov 24 21:01:06 2011 +0100
    11.3 @@ -91,7 +91,7 @@
    11.4  val simproc = Simplifier.simproc_global @{theory}
    11.5    "add_ac_proc" ["x + y::'a::ab_semigroup_add"] ((K o K) solve);
    11.6  
    11.7 -val cancel_ss = HOL_basic_ss settermless less_agrp
    11.8 +val cancel_ss = (HOL_basic_ss |> Simplifier.set_termless less_agrp)
    11.9    addsimprocs [simproc] addsimps
   11.10    [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_minus},
   11.11     @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
    12.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Nov 24 20:45:34 2011 +0100
    12.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Nov 24 21:01:06 2011 +0100
    12.3 @@ -704,8 +704,9 @@
    12.4  
    12.5  local
    12.6    val nnf_simpset =
    12.7 -    empty_ss setmkeqTrue mk_eq_True
    12.8 -    setmksimps (mksimps mksimps_pairs)
    12.9 +    (empty_ss
   12.10 +      |> Simplifier.set_mkeqTrue mk_eq_True
   12.11 +      |> Simplifier.set_mksimps (mksimps mksimps_pairs))
   12.12      addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
   12.13        @{thm de_Morgan_conj}, not_all, not_ex, not_not]
   12.14    fun prem_nnf_tac ss = full_simp_tac (Simplifier.inherit_context ss nnf_simpset)
   12.15 @@ -838,8 +839,9 @@
   12.16  
   12.17  local
   12.18    val nnf_simpset =
   12.19 -    empty_ss setmkeqTrue mk_eq_True
   12.20 -    setmksimps (mksimps mksimps_pairs)
   12.21 +    (empty_ss
   12.22 +      |> Simplifier.set_mkeqTrue mk_eq_True
   12.23 +      |> Simplifier.set_mksimps (mksimps mksimps_pairs))
   12.24      addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
   12.25        @{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}];
   12.26    fun prem_nnf_tac i st =
    13.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Thu Nov 24 20:45:34 2011 +0100
    13.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Nov 24 21:01:06 2011 +0100
    13.3 @@ -169,7 +169,7 @@
    13.4  
    13.5  fun numtermless tu = (numterm_ord tu = LESS);
    13.6  
    13.7 -val num_ss = HOL_ss settermless numtermless;
    13.8 +val num_ss = HOL_ss |> Simplifier.set_termless numtermless;
    13.9  
   13.10  (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
   13.11  val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
    14.1 --- a/src/HOL/Tools/simpdata.ML	Thu Nov 24 20:45:34 2011 +0100
    14.2 +++ b/src/HOL/Tools/simpdata.ML	Thu Nov 24 21:01:06 2011 +0100
    14.3 @@ -167,12 +167,12 @@
    14.4  
    14.5  val HOL_basic_ss =
    14.6    Simplifier.global_context @{theory} empty_ss
    14.7 -    setsubgoaler asm_simp_tac
    14.8 -    setSSolver safe_solver
    14.9 -    setSolver unsafe_solver
   14.10 -    setmksimps (mksimps mksimps_pairs)
   14.11 -    setmkeqTrue mk_eq_True
   14.12 -    setmkcong mk_meta_cong;
   14.13 +  setSSolver safe_solver
   14.14 +  setSolver unsafe_solver
   14.15 +  |> Simplifier.set_subgoaler asm_simp_tac
   14.16 +  |> Simplifier.set_mksimps (mksimps mksimps_pairs)
   14.17 +  |> Simplifier.set_mkeqTrue mk_eq_True
   14.18 +  |> Simplifier.set_mkcong mk_meta_cong;
   14.19  
   14.20  fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
   14.21  
    15.1 --- a/src/Provers/hypsubst.ML	Thu Nov 24 20:45:34 2011 +0100
    15.2 +++ b/src/Provers/hypsubst.ML	Thu Nov 24 21:01:06 2011 +0100
    15.3 @@ -131,7 +131,7 @@
    15.4        let
    15.5          val (k, _) = eq_var bnd true Bi
    15.6          val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
    15.7 -          setmksimps (K (mk_eqs bnd))
    15.8 +          |> Simplifier.set_mksimps (K (mk_eqs bnd))
    15.9        in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
   15.10          etac thin_rl i, rotate_tac (~k) i]
   15.11        end handle THM _ => no_tac | EQ_VAR => no_tac) i st
    16.1 --- a/src/Pure/raw_simplifier.ML	Thu Nov 24 20:45:34 2011 +0100
    16.2 +++ b/src/Pure/raw_simplifier.ML	Thu Nov 24 21:01:06 2011 +0100
    16.3 @@ -6,8 +6,8 @@
    16.4  
    16.5  infix 4
    16.6    addsimps delsimps addsimprocs delsimprocs
    16.7 -  setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
    16.8 -  setloop' setloop addloop addloop' delloop setSSolver addSSolver setSolver addSolver;
    16.9 +  setloop' setloop addloop addloop' delloop
   16.10 +  setSSolver addSSolver setSolver addSolver;
   16.11  
   16.12  signature BASIC_RAW_SIMPLIFIER =
   16.13  sig
   16.14 @@ -41,13 +41,6 @@
   16.15    val delsimps: simpset * thm list -> simpset
   16.16    val addsimprocs: simpset * simproc list -> simpset
   16.17    val delsimprocs: simpset * simproc list -> simpset
   16.18 -  val mksimps: simpset -> thm -> thm list
   16.19 -  val setmksimps: simpset * (simpset -> thm -> thm list) -> simpset
   16.20 -  val setmkcong: simpset * (simpset -> thm -> thm) -> simpset
   16.21 -  val setmksym: simpset * (simpset -> thm -> thm option) -> simpset
   16.22 -  val setmkeqTrue: simpset * (simpset -> thm -> thm option) -> simpset
   16.23 -  val settermless: simpset * (term * term -> bool) -> simpset
   16.24 -  val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
   16.25    val setloop': simpset * (simpset -> int -> tactic) -> simpset
   16.26    val setloop: simpset * (int -> tactic) -> simpset
   16.27    val addloop': simpset * (string * (simpset -> int -> tactic)) -> simpset
   16.28 @@ -99,6 +92,13 @@
   16.29    val del_eqcong: thm -> simpset -> simpset
   16.30    val add_cong: thm -> simpset -> simpset
   16.31    val del_cong: thm -> simpset -> simpset
   16.32 +  val mksimps: simpset -> thm -> thm list
   16.33 +  val set_mksimps: (simpset -> thm -> thm list) -> simpset -> simpset
   16.34 +  val set_mkcong: (simpset -> thm -> thm) -> simpset -> simpset
   16.35 +  val set_mksym: (simpset -> thm -> thm option) -> simpset -> simpset
   16.36 +  val set_mkeqTrue: (simpset -> thm -> thm option) -> simpset -> simpset
   16.37 +  val set_termless: (term * term -> bool) -> simpset -> simpset
   16.38 +  val set_subgoaler: (simpset -> int -> tactic) -> simpset -> simpset
   16.39    val solver: simpset -> solver -> int -> tactic
   16.40    val simp_depth_limit_raw: Config.raw
   16.41    val clear_ss: simpset -> simpset
   16.42 @@ -685,16 +685,16 @@
   16.43  
   16.44  fun mksimps (ss as Simpset (_, {mk_rews = {mk, ...}, ...})) = mk ss;
   16.45  
   16.46 -fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
   16.47 +fun set_mksimps mk = map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
   16.48    (mk, mk_cong, mk_sym, mk_eq_True, reorient));
   16.49  
   16.50 -fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) =>
   16.51 +fun set_mkcong mk_cong = map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) =>
   16.52    (mk, mk_cong, mk_sym, mk_eq_True, reorient));
   16.53  
   16.54 -fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) =>
   16.55 +fun set_mksym mk_sym = map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) =>
   16.56    (mk, mk_cong, mk_sym, mk_eq_True, reorient));
   16.57  
   16.58 -fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) =>
   16.59 +fun set_mkeqTrue mk_eq_True = map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) =>
   16.60    (mk, mk_cong, mk_sym, mk_eq_True, reorient));
   16.61  
   16.62  fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) =>
   16.63 @@ -705,14 +705,14 @@
   16.64  
   16.65  (* termless *)
   16.66  
   16.67 -fun ss settermless termless = ss |>
   16.68 +fun set_termless termless =
   16.69    map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
   16.70     (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
   16.71  
   16.72  
   16.73  (* tactics *)
   16.74  
   16.75 -fun ss setsubgoaler subgoal_tac = ss |>
   16.76 +fun set_subgoaler subgoal_tac =
   16.77    map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
   16.78     (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
   16.79  
    17.1 --- a/src/Pure/simplifier.ML	Thu Nov 24 20:45:34 2011 +0100
    17.2 +++ b/src/Pure/simplifier.ML	Thu Nov 24 21:01:06 2011 +0100
    17.3 @@ -42,6 +42,13 @@
    17.4    val add_cong: thm -> simpset -> simpset
    17.5    val del_cong: thm -> simpset -> simpset
    17.6    val add_prems: thm list -> simpset -> simpset
    17.7 +  val mksimps: simpset -> thm -> thm list
    17.8 +  val set_mksimps: (simpset -> thm -> thm list) -> simpset -> simpset
    17.9 +  val set_mkcong: (simpset -> thm -> thm) -> simpset -> simpset
   17.10 +  val set_mksym: (simpset -> thm -> thm option) -> simpset -> simpset
   17.11 +  val set_mkeqTrue: (simpset -> thm -> thm option) -> simpset -> simpset
   17.12 +  val set_termless: (term * term -> bool) -> simpset -> simpset
   17.13 +  val set_subgoaler: (simpset -> int -> tactic) -> simpset -> simpset
   17.14    val inherit_context: simpset -> simpset -> simpset
   17.15    val the_context: simpset -> Proof.context
   17.16    val context: Proof.context -> simpset -> simpset
   17.17 @@ -415,10 +422,11 @@
   17.18  
   17.19      fun mksimps thm = mk_eq (Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm);
   17.20    in
   17.21 -    empty_ss setsubgoaler asm_simp_tac
   17.22 +    empty_ss
   17.23      setSSolver safe_solver
   17.24      setSolver unsafe_solver
   17.25 -    setmksimps (K mksimps)
   17.26 +    |> set_subgoaler asm_simp_tac
   17.27 +    |> set_mksimps (K mksimps)
   17.28    end));
   17.29  
   17.30  end;
    18.1 --- a/src/Sequents/simpdata.ML	Thu Nov 24 20:45:34 2011 +0100
    18.2 +++ b/src/Sequents/simpdata.ML	Thu Nov 24 21:01:06 2011 +0100
    18.3 @@ -68,11 +68,11 @@
    18.4  (*No simprules, but basic infrastructure for simplification*)
    18.5  val LK_basic_ss =
    18.6    Simplifier.global_context @{theory} empty_ss
    18.7 -    setsubgoaler asm_simp_tac
    18.8 -    setSSolver (mk_solver "safe" safe_solver)
    18.9 -    setSolver (mk_solver "unsafe" unsafe_solver)
   18.10 -    setmksimps (K (map mk_meta_eq o atomize o gen_all))
   18.11 -    setmkcong mk_meta_cong;
   18.12 +  setSSolver (mk_solver "safe" safe_solver)
   18.13 +  setSolver (mk_solver "unsafe" unsafe_solver)
   18.14 +  |> Simplifier.set_subgoaler asm_simp_tac
   18.15 +  |> Simplifier.set_mksimps (K (map mk_meta_eq o atomize o gen_all))
   18.16 +  |> Simplifier.set_mkcong mk_meta_cong;
   18.17  
   18.18  val LK_simps =
   18.19     [triv_forall_equality, (* prunes params *)
    19.1 --- a/src/ZF/Main_ZF.thy	Thu Nov 24 20:45:34 2011 +0100
    19.2 +++ b/src/ZF/Main_ZF.thy	Thu Nov 24 21:01:06 2011 +0100
    19.3 @@ -71,7 +71,7 @@
    19.4  
    19.5  
    19.6  declaration {* fn _ =>
    19.7 -  Simplifier.map_ss (fn ss => ss setmksimps (K (map mk_eq o Ord_atomize o gen_all)))
    19.8 +  Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all)))
    19.9  *}
   19.10  
   19.11  end
    20.1 --- a/src/ZF/OrdQuant.thy	Thu Nov 24 20:45:34 2011 +0100
    20.2 +++ b/src/ZF/OrdQuant.thy	Thu Nov 24 21:01:06 2011 +0100
    20.3 @@ -363,7 +363,7 @@
    20.4               ZF_mem_pairs);
    20.5  *}
    20.6  declaration {* fn _ =>
    20.7 -  Simplifier.map_ss (fn ss => ss setmksimps (K (map mk_eq o Ord_atomize o gen_all)))
    20.8 +  Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all)))
    20.9  *}
   20.10  
   20.11  text {* Setting up the one-point-rule simproc *}
    21.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Nov 24 20:45:34 2011 +0100
    21.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Nov 24 21:01:06 2011 +0100
    21.3 @@ -326,8 +326,9 @@
    21.4  
    21.5       (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
    21.6         If the premises get simplified, then the proofs could fail.*)
    21.7 -     val min_ss = Simplifier.global_context thy empty_ss
    21.8 -           setmksimps (K (map mk_eq o ZF_atomize o gen_all))
    21.9 +     val min_ss =
   21.10 +           (Simplifier.global_context thy empty_ss
   21.11 +             |> Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)))
   21.12             setSolver (mk_solver "minimal"
   21.13                        (fn ss => resolve_tac (triv_rls @ Simplifier.prems_of ss)
   21.14                                     ORELSE' assume_tac
    22.1 --- a/src/ZF/pair.thy	Thu Nov 24 20:45:34 2011 +0100
    22.2 +++ b/src/ZF/pair.thy	Thu Nov 24 21:01:06 2011 +0100
    22.3 @@ -10,9 +10,9 @@
    22.4  begin
    22.5  
    22.6  setup {*
    22.7 -  Simplifier.map_simpset_global (fn ss =>
    22.8 -    ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
    22.9 -    |> Simplifier.add_cong @{thm if_weak_cong})
   22.10 +  Simplifier.map_simpset_global
   22.11 +    (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all))
   22.12 +      #> Simplifier.add_cong @{thm if_weak_cong})
   22.13  *}
   22.14  
   22.15  ML {* val ZF_ss = @{simpset} *}