1.1 --- a/src/FOL/simpdata.ML	Thu Apr 29 22:08:57 2010 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu Apr 29 22:56:32 2010 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4        (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
     1.5  
     1.6  (*Congruence rules for = or <-> (instead of ==)*)
     1.7 -fun mk_meta_cong rl =
     1.8 +fun mk_meta_cong (_: simpset) rl =
     1.9    Drule.export_without_context (mk_meta_eq (mk_meta_prems rl))
    1.10      handle THM _ =>
    1.11        error("Premises and conclusion of congruence rules must use =-equality or <->");
    1.12 @@ -52,7 +52,7 @@
    1.13           | _ => [th])
    1.14    in atoms end;
    1.15  
    1.16 -fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
    1.17 +fun mksimps pairs (_: simpset) = map mk_eq o mk_atomize pairs o gen_all;
    1.18  
    1.19  
    1.20  (** make simplification procedures for quantifier elimination **)

     2.1 --- a/src/HOL/HOL.thy	Thu Apr 29 22:08:57 2010 +0200
     2.2 +++ b/src/HOL/HOL.thy	Thu Apr 29 22:56:32 2010 +0200
     2.3 @@ -1491,7 +1491,7 @@
     2.4  setup {*
     2.5    Induct.setup #>
     2.6    Context.theory_map (Induct.map_simpset (fn ss => ss
     2.7 -    setmksimps (Simpdata.mksimps Simpdata.mksimps_pairs #>
     2.8 +    setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
     2.9        map (Simplifier.rewrite_rule (map Thm.symmetric
    2.10          @{thms induct_rulify_fallback induct_true_def induct_false_def})))
    2.11      addsimprocs

     3.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Apr 29 22:08:57 2010 +0200
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Apr 29 22:56:32 2010 +0200
     3.3 @@ -1249,7 +1249,7 @@
     3.4      let
     3.5          val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
     3.6          val hol4ss = Simplifier.global_context thy empty_ss
     3.7 -          setmksimps single addsimps hol4rews1
     3.8 +          setmksimps (K single) addsimps hol4rews1
     3.9      in
    3.10          Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
    3.11      end

     4.1 --- a/src/HOL/Import/shuffler.ML	Thu Apr 29 22:08:57 2010 +0200
     4.2 +++ b/src/HOL/Import/shuffler.ML	Thu Apr 29 22:56:32 2010 +0200
     4.3 @@ -489,7 +489,7 @@
     4.4      let
     4.5          val norms = ShuffleData.get thy
     4.6          val ss = Simplifier.global_context thy empty_ss
     4.7 -          setmksimps single
     4.8 +          setmksimps (K single)
     4.9            addsimps (map (Thm.transfer thy) norms)
    4.10            addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
    4.11          fun chain f th =

     5.1 --- a/src/HOL/Tools/simpdata.ML	Thu Apr 29 22:08:57 2010 +0200
     5.2 +++ b/src/HOL/Tools/simpdata.ML	Thu Apr 29 22:56:32 2010 +0200
     5.3 @@ -48,7 +48,7 @@
     5.4     | _ $ (Const (@{const_name "Not"}, _) $ _) => th RS @{thm Eq_FalseI}
     5.5     | _ => th RS @{thm Eq_TrueI}
     5.6  
     5.7 -fun mk_eq_True r =
     5.8 +fun mk_eq_True (_: simpset) r =
     5.9    SOME (r RS @{thm meta_eq_to_obj_eq} RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE;
    5.10  
    5.11  (* Produce theorems of the form
    5.12 @@ -80,7 +80,7 @@
    5.13    end;
    5.14  
    5.15  (*Congruence rules for = (instead of ==)*)
    5.16 -fun mk_meta_cong rl = zero_var_indexes
    5.17 +fun mk_meta_cong (_: simpset) rl = zero_var_indexes
    5.18    (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
    5.19       rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
    5.20     in mk_meta_eq rl' handle THM _ =>
    5.21 @@ -107,7 +107,7 @@
    5.22        end;
    5.23    in atoms end;
    5.24  
    5.25 -fun mksimps pairs =
    5.26 +fun mksimps pairs (_: simpset) =
    5.27    map_filter (try mk_eq) o mk_atomize pairs o gen_all;
    5.28  
    5.29  fun unsafe_solver_tac prems =

     6.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Apr 29 22:08:57 2010 +0200
     6.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Apr 29 22:56:32 2010 +0200
     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 NONE)) *}
     6.8 +declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (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 (SOME o symmetric_fun)) *}
    6.17 +declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K (SOME o symmetric_fun))) *}
    6.18  
    6.19  
    6.20  end

     7.1 --- a/src/Provers/hypsubst.ML	Thu Apr 29 22:08:57 2010 +0200
     7.2 +++ b/src/Provers/hypsubst.ML	Thu Apr 29 22:56:32 2010 +0200
     7.3 @@ -156,7 +156,7 @@
     7.4        let
     7.5          val (k, _) = eq_var bnd true Bi
     7.6          val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
     7.7 -          setmksimps (mk_eqs bnd)
     7.8 +          setmksimps (K (mk_eqs bnd))
     7.9        in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
    7.10          etac thin_rl i, rotate_tac (~k) i]
    7.11        end handle THM _ => no_tac | EQ_VAR => no_tac) i st

     8.1 --- a/src/Pure/meta_simplifier.ML	Thu Apr 29 22:08:57 2010 +0200
     8.2 +++ b/src/Pure/meta_simplifier.ML	Thu Apr 29 22:56:32 2010 +0200
     8.3 @@ -51,10 +51,10 @@
     8.4    val addsimprocs: simpset * simproc list -> simpset
     8.5    val delsimprocs: simpset * simproc list -> simpset
     8.6    val mksimps: simpset -> thm -> thm list
     8.7 -  val setmksimps: simpset * (thm -> thm list) -> simpset
     8.8 -  val setmkcong: simpset * (thm -> thm) -> simpset
     8.9 -  val setmksym: simpset * (thm -> thm option) -> simpset
    8.10 -  val setmkeqTrue: simpset * (thm -> thm option) -> simpset
    8.11 +  val setmksimps: simpset * (simpset -> thm -> thm list) -> simpset
    8.12 +  val setmkcong: simpset * (simpset -> thm -> thm) -> simpset
    8.13 +  val setmksym: simpset * (simpset -> thm -> thm option) -> simpset
    8.14 +  val setmkeqTrue: simpset * (simpset -> thm -> thm option) -> simpset
    8.15    val settermless: simpset * (term * term -> bool) -> simpset
    8.16    val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
    8.17    val setloop': simpset * (simpset -> int -> tactic) -> simpset
    8.18 @@ -92,10 +92,10 @@
    8.19     {congs: (string * thm) list * string list,
    8.20      procs: proc Net.net,
    8.21      mk_rews:
    8.22 -     {mk: thm -> thm list,
    8.23 -      mk_cong: thm -> thm,
    8.24 -      mk_sym: thm -> thm option,
    8.25 -      mk_eq_True: thm -> thm option,
    8.26 +     {mk: simpset -> thm -> thm list,
    8.27 +      mk_cong: simpset -> thm -> thm,
    8.28 +      mk_sym: simpset -> thm -> thm option,
    8.29 +      mk_eq_True: simpset -> thm -> thm option,
    8.30        reorient: theory -> term list -> term -> term -> bool},
    8.31      termless: term * term -> bool,
    8.32      subgoal_tac: simpset -> int -> tactic,
    8.33 @@ -181,13 +181,6 @@
    8.34        mk_eq_True: turn P into P == True;
    8.35      termless: relation for ordered rewriting;*)
    8.36  
    8.37 -type mk_rews =
    8.38 - {mk: thm -> thm list,
    8.39 -  mk_cong: thm -> thm,
    8.40 -  mk_sym: thm -> thm option,
    8.41 -  mk_eq_True: thm -> thm option,
    8.42 -  reorient: theory -> term list -> term -> term -> bool};
    8.43 -
    8.44  datatype simpset =
    8.45    Simpset of
    8.46     {rules: rrule Net.net,
    8.47 @@ -197,7 +190,12 @@
    8.48      context: Proof.context option} *
    8.49     {congs: (string * thm) list * string list,
    8.50      procs: proc Net.net,
    8.51 -    mk_rews: mk_rews,
    8.52 +    mk_rews:
    8.53 +     {mk: simpset -> thm -> thm list,
    8.54 +      mk_cong: simpset -> thm -> thm,
    8.55 +      mk_sym: simpset -> thm -> thm option,
    8.56 +      mk_eq_True: simpset -> thm -> thm option,
    8.57 +      reorient: theory -> term list -> term -> term -> bool},
    8.58      termless: term * term -> bool,
    8.59      subgoal_tac: simpset -> int -> tactic,
    8.60      loop_tacs: (string * (simpset -> int -> tactic)) list,
    8.61 @@ -458,8 +456,8 @@
    8.62      else (lhs, rhs)
    8.63    end;
    8.64  
    8.65 -fun mk_eq_True (Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
    8.66 -  (case mk_eq_True thm of
    8.67 +fun mk_eq_True (ss as Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
    8.68 +  (case mk_eq_True ss thm of
    8.69      NONE => []
    8.70    | SOME eq_True =>
    8.71        let
    8.72 @@ -495,7 +493,7 @@
    8.73        if reorient thy prems rhs lhs
    8.74        then mk_eq_True ss (thm, name)
    8.75        else
    8.76 -        (case mk_sym thm of
    8.77 +        (case mk_sym ss thm of
    8.78            NONE => []
    8.79          | SOME thm' =>
    8.80              let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
    8.81 @@ -503,8 +501,8 @@
    8.82      else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
    8.83    end;
    8.84  
    8.85 -fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
    8.86 -  maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk thm)) thms;
    8.87 +fun extract_rews (ss as Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
    8.88 +  maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ss thm)) thms;
    8.89  
    8.90  fun extract_safe_rrules (ss, thm) =
    8.91    maps (orient_rrule ss) (extract_rews (ss, [thm]));
    8.92 @@ -588,7 +586,7 @@
    8.93          if is_full_cong thm then NONE else SOME a);
    8.94      in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
    8.95  
    8.96 -fun mk_cong (Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f;
    8.97 +fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss;
    8.98  
    8.99  in
   8.100  
   8.101 @@ -674,7 +672,7 @@
   8.102  
   8.103  in
   8.104  
   8.105 -fun mksimps (Simpset (_, {mk_rews = {mk, ...}, ...})) = mk;
   8.106 +fun mksimps (ss as Simpset (_, {mk_rews = {mk, ...}, ...})) = mk ss;
   8.107  
   8.108  fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
   8.109    (mk, mk_cong, mk_sym, mk_eq_True, reorient));
   8.110 @@ -762,14 +760,14 @@
   8.111    init_ss mk_rews termless subgoal_tac solvers
   8.112    |> inherit_context ss;
   8.113  
   8.114 -val basic_mk_rews: mk_rews =
   8.115 - {mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
   8.116 -  mk_cong = I,
   8.117 -  mk_sym = SOME o Drule.symmetric_fun,
   8.118 -  mk_eq_True = K NONE,
   8.119 -  reorient = default_reorient};
   8.120 -
   8.121 -val empty_ss = init_ss basic_mk_rews Term_Ord.termless (K (K no_tac)) ([], []);
   8.122 +val empty_ss =
   8.123 +  init_ss
   8.124 +    {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
   8.125 +      mk_cong = K I,
   8.126 +      mk_sym = K (SOME o Drule.symmetric_fun),
   8.127 +      mk_eq_True = K (K NONE),
   8.128 +      reorient = default_reorient}
   8.129 +    Term_Ord.termless (K (K no_tac)) ([], []);
   8.130  
   8.131  
   8.132  (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)

     9.1 --- a/src/Pure/simplifier.ML	Thu Apr 29 22:08:57 2010 +0200
     9.2 +++ b/src/Pure/simplifier.ML	Thu Apr 29 22:56:32 2010 +0200
     9.3 @@ -411,7 +411,7 @@
     9.4      empty_ss setsubgoaler asm_simp_tac
     9.5      setSSolver safe_solver
     9.6      setSolver unsafe_solver
     9.7 -    setmksimps mksimps
     9.8 +    setmksimps (K mksimps)
     9.9    end));
    9.10  
    9.11  end;

    10.1 --- a/src/Sequents/simpdata.ML	Thu Apr 29 22:08:57 2010 +0200
    10.2 +++ b/src/Sequents/simpdata.ML	Thu Apr 29 22:56:32 2010 +0200
    10.3 @@ -47,7 +47,7 @@
    10.4        (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
    10.5  
    10.6  (*Congruence rules for = or <-> (instead of ==)*)
    10.7 -fun mk_meta_cong rl =
    10.8 +fun mk_meta_cong (_: simpset) rl =
    10.9    Drule.export_without_context(mk_meta_eq (mk_meta_prems rl))
   10.10      handle THM _ =>
   10.11        error("Premises and conclusion of congruence rules must use =-equality or <->");
   10.12 @@ -71,7 +71,7 @@
   10.13      setsubgoaler asm_simp_tac
   10.14      setSSolver (mk_solver "safe" safe_solver)
   10.15      setSolver (mk_solver "unsafe" unsafe_solver)
   10.16 -    setmksimps (map mk_meta_eq o atomize o gen_all)
   10.17 +    setmksimps (K (map mk_meta_eq o atomize o gen_all))
   10.18      setmkcong mk_meta_cong;
   10.19  
   10.20  val LK_simps =

    11.1 --- a/src/ZF/Main_ZF.thy	Thu Apr 29 22:08:57 2010 +0200
    11.2 +++ b/src/ZF/Main_ZF.thy	Thu Apr 29 22:56:32 2010 +0200
    11.3 @@ -71,7 +71,7 @@
    11.4  
    11.5  
    11.6  declaration {* fn _ =>
    11.7 -  Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
    11.8 +  Simplifier.map_ss (fn ss => ss setmksimps (K (map mk_eq o Ord_atomize o gen_all)))
    11.9  *}
   11.10  
   11.11  end

    12.1 --- a/src/ZF/OrdQuant.thy	Thu Apr 29 22:08:57 2010 +0200
    12.2 +++ b/src/ZF/OrdQuant.thy	Thu Apr 29 22:56:32 2010 +0200
    12.3 @@ -363,7 +363,7 @@
    12.4               ZF_mem_pairs);
    12.5  *}
    12.6  declaration {* fn _ =>
    12.7 -  Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
    12.8 +  Simplifier.map_ss (fn ss => ss setmksimps (K (map mk_eq o Ord_atomize o gen_all)))
    12.9  *}
   12.10  
   12.11  text {* Setting up the one-point-rule simproc *}

    13.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Apr 29 22:08:57 2010 +0200
    13.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Apr 29 22:56:32 2010 +0200
    13.3 @@ -328,7 +328,7 @@
    13.4       (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
    13.5         If the premises get simplified, then the proofs could fail.*)
    13.6       val min_ss = Simplifier.global_context thy empty_ss
    13.7 -           setmksimps (map mk_eq o ZF_atomize o gen_all)
    13.8 +           setmksimps (K (map mk_eq o ZF_atomize o gen_all))
    13.9             setSolver (mk_solver "minimal"
   13.10                        (fn prems => resolve_tac (triv_rls@prems)
   13.11                                     ORELSE' assume_tac

    14.1 --- a/src/ZF/simpdata.ML	Thu Apr 29 22:08:57 2010 +0200
    14.2 +++ b/src/ZF/simpdata.ML	Thu Apr 29 22:56:32 2010 +0200
    14.3 @@ -44,7 +44,7 @@
    14.4  val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
    14.5  
    14.6  change_simpset (fn ss =>
    14.7 -  ss setmksimps (map mk_eq o ZF_atomize o gen_all)
    14.8 +  ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
    14.9    addcongs [@{thm if_weak_cong}]);
   14.10  
   14.11  local