# HG changeset patch
# User wenzelm
# Date 1272574592 -7200
# Node ID 0e7fc5bf38de809757fb8dbf142d1bec0586e4c0
# Parent  7cb6b40d19b21411d287d9a9d02e88ae23065ced
proper context for mksimps etc. -- via simpset of the running Simplifier;

diff -r 7cb6b40d19b2 -r 0e7fc5bf38de src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/FOL/simpdata.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -26,7 +26,7 @@
       (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
 
 (*Congruence rules for = or <-> (instead of ==)*)
-fun mk_meta_cong rl =
+fun mk_meta_cong (_: simpset) rl =
   Drule.export_without_context (mk_meta_eq (mk_meta_prems rl))
     handle THM _ =>
       error("Premises and conclusion of congruence rules must use =-equality or <->");
@@ -52,7 +52,7 @@
          | _ => [th])
   in atoms end;
 
-fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
+fun mksimps pairs (_: simpset) = map mk_eq o mk_atomize pairs o gen_all;
 
 
 (** make simplification procedures for quantifier elimination **)
diff -r 7cb6b40d19b2 -r 0e7fc5bf38de src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/HOL/HOL.thy	Thu Apr 29 22:56:32 2010 +0200
@@ -1491,7 +1491,7 @@
 setup {*
   Induct.setup #>
   Context.theory_map (Induct.map_simpset (fn ss => ss
-    setmksimps (Simpdata.mksimps Simpdata.mksimps_pairs #>
+    setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
       map (Simplifier.rewrite_rule (map Thm.symmetric
         @{thms induct_rulify_fallback induct_true_def induct_false_def})))
     addsimprocs
diff -r 7cb6b40d19b2 -r 0e7fc5bf38de src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -1249,7 +1249,7 @@
     let
         val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
         val hol4ss = Simplifier.global_context thy empty_ss
-          setmksimps single addsimps hol4rews1
+          setmksimps (K single) addsimps hol4rews1
     in
         Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
     end
diff -r 7cb6b40d19b2 -r 0e7fc5bf38de src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/HOL/Import/shuffler.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -489,7 +489,7 @@
     let
         val norms = ShuffleData.get thy
         val ss = Simplifier.global_context thy empty_ss
-          setmksimps single
+          setmksimps (K single)
           addsimps (map (Thm.transfer thy) norms)
           addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
         fun chain f th =
diff -r 7cb6b40d19b2 -r 0e7fc5bf38de src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -48,7 +48,7 @@
    | _ $ (Const (@{const_name "Not"}, _) $ _) => th RS @{thm Eq_FalseI}
    | _ => th RS @{thm Eq_TrueI}
 
-fun mk_eq_True r =
+fun mk_eq_True (_: simpset) r =
   SOME (r RS @{thm meta_eq_to_obj_eq} RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE;
 
 (* Produce theorems of the form
@@ -80,7 +80,7 @@
   end;
 
 (*Congruence rules for = (instead of ==)*)
-fun mk_meta_cong rl = zero_var_indexes
+fun mk_meta_cong (_: simpset) rl = zero_var_indexes
   (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
      rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
    in mk_meta_eq rl' handle THM _ =>
@@ -107,7 +107,7 @@
       end;
   in atoms end;
 
-fun mksimps pairs =
+fun mksimps pairs (_: simpset) =
   map_filter (try mk_eq) o mk_atomize pairs o gen_all;
 
 fun unsafe_solver_tac prems =
diff -r 7cb6b40d19b2 -r 0e7fc5bf38de src/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Apr 29 22:56:32 2010 +0200
@@ -67,7 +67,7 @@
   "Finite (mksch A B$tr$x$y) --> Finite tr"
 
 
-declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K NONE)) *}
+declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K (K NONE))) *}
 
 
 subsection "mksch rewrite rules"
@@ -967,7 +967,7 @@
 done
 
 
-declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (SOME o symmetric_fun)) *}
+declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K (SOME o symmetric_fun))) *}
 
 
 end
diff -r 7cb6b40d19b2 -r 0e7fc5bf38de src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/Provers/hypsubst.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -156,7 +156,7 @@
       let
         val (k, _) = eq_var bnd true Bi
         val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
-          setmksimps (mk_eqs bnd)
+          setmksimps (K (mk_eqs bnd))
       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
         etac thin_rl i, rotate_tac (~k) i]
       end handle THM _ => no_tac | EQ_VAR => no_tac) i st
diff -r 7cb6b40d19b2 -r 0e7fc5bf38de src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -51,10 +51,10 @@
   val addsimprocs: simpset * simproc list -> simpset
   val delsimprocs: simpset * simproc list -> simpset
   val mksimps: simpset -> thm -> thm list
-  val setmksimps: simpset * (thm -> thm list) -> simpset
-  val setmkcong: simpset * (thm -> thm) -> simpset
-  val setmksym: simpset * (thm -> thm option) -> simpset
-  val setmkeqTrue: simpset * (thm -> thm option) -> simpset
+  val setmksimps: simpset * (simpset -> thm -> thm list) -> simpset
+  val setmkcong: simpset * (simpset -> thm -> thm) -> simpset
+  val setmksym: simpset * (simpset -> thm -> thm option) -> simpset
+  val setmkeqTrue: simpset * (simpset -> thm -> thm option) -> simpset
   val settermless: simpset * (term * term -> bool) -> simpset
   val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
   val setloop': simpset * (simpset -> int -> tactic) -> simpset
@@ -92,10 +92,10 @@
    {congs: (string * thm) list * string list,
     procs: proc Net.net,
     mk_rews:
-     {mk: thm -> thm list,
-      mk_cong: thm -> thm,
-      mk_sym: thm -> thm option,
-      mk_eq_True: thm -> thm option,
+     {mk: simpset -> thm -> thm list,
+      mk_cong: simpset -> thm -> thm,
+      mk_sym: simpset -> thm -> thm option,
+      mk_eq_True: simpset -> thm -> thm option,
       reorient: theory -> term list -> term -> term -> bool},
     termless: term * term -> bool,
     subgoal_tac: simpset -> int -> tactic,
@@ -181,13 +181,6 @@
       mk_eq_True: turn P into P == True;
     termless: relation for ordered rewriting;*)
 
-type mk_rews =
- {mk: thm -> thm list,
-  mk_cong: thm -> thm,
-  mk_sym: thm -> thm option,
-  mk_eq_True: thm -> thm option,
-  reorient: theory -> term list -> term -> term -> bool};
-
 datatype simpset =
   Simpset of
    {rules: rrule Net.net,
@@ -197,7 +190,12 @@
     context: Proof.context option} *
    {congs: (string * thm) list * string list,
     procs: proc Net.net,
-    mk_rews: mk_rews,
+    mk_rews:
+     {mk: simpset -> thm -> thm list,
+      mk_cong: simpset -> thm -> thm,
+      mk_sym: simpset -> thm -> thm option,
+      mk_eq_True: simpset -> thm -> thm option,
+      reorient: theory -> term list -> term -> term -> bool},
     termless: term * term -> bool,
     subgoal_tac: simpset -> int -> tactic,
     loop_tacs: (string * (simpset -> int -> tactic)) list,
@@ -458,8 +456,8 @@
     else (lhs, rhs)
   end;
 
-fun mk_eq_True (Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
-  (case mk_eq_True thm of
+fun mk_eq_True (ss as Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
+  (case mk_eq_True ss thm of
     NONE => []
   | SOME eq_True =>
       let
@@ -495,7 +493,7 @@
       if reorient thy prems rhs lhs
       then mk_eq_True ss (thm, name)
       else
-        (case mk_sym thm of
+        (case mk_sym ss thm of
           NONE => []
         | SOME thm' =>
             let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
@@ -503,8 +501,8 @@
     else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
   end;
 
-fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
-  maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk thm)) thms;
+fun extract_rews (ss as Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
+  maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ss thm)) thms;
 
 fun extract_safe_rrules (ss, thm) =
   maps (orient_rrule ss) (extract_rews (ss, [thm]));
@@ -588,7 +586,7 @@
         if is_full_cong thm then NONE else SOME a);
     in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
 
-fun mk_cong (Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f;
+fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss;
 
 in
 
@@ -674,7 +672,7 @@
 
 in
 
-fun mksimps (Simpset (_, {mk_rews = {mk, ...}, ...})) = mk;
+fun mksimps (ss as Simpset (_, {mk_rews = {mk, ...}, ...})) = mk ss;
 
 fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
@@ -762,14 +760,14 @@
   init_ss mk_rews termless subgoal_tac solvers
   |> inherit_context ss;
 
-val basic_mk_rews: mk_rews =
- {mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
-  mk_cong = I,
-  mk_sym = SOME o Drule.symmetric_fun,
-  mk_eq_True = K NONE,
-  reorient = default_reorient};
-
-val empty_ss = init_ss basic_mk_rews Term_Ord.termless (K (K no_tac)) ([], []);
+val empty_ss =
+  init_ss
+    {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
+      mk_cong = K I,
+      mk_sym = K (SOME o Drule.symmetric_fun),
+      mk_eq_True = K (K NONE),
+      reorient = default_reorient}
+    Term_Ord.termless (K (K no_tac)) ([], []);
 
 
 (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)
diff -r 7cb6b40d19b2 -r 0e7fc5bf38de src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/Pure/simplifier.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -411,7 +411,7 @@
     empty_ss setsubgoaler asm_simp_tac
     setSSolver safe_solver
     setSolver unsafe_solver
-    setmksimps mksimps
+    setmksimps (K mksimps)
   end));
 
 end;
diff -r 7cb6b40d19b2 -r 0e7fc5bf38de src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/Sequents/simpdata.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -47,7 +47,7 @@
       (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
 
 (*Congruence rules for = or <-> (instead of ==)*)
-fun mk_meta_cong rl =
+fun mk_meta_cong (_: simpset) rl =
   Drule.export_without_context(mk_meta_eq (mk_meta_prems rl))
     handle THM _ =>
       error("Premises and conclusion of congruence rules must use =-equality or <->");
@@ -71,7 +71,7 @@
     setsubgoaler asm_simp_tac
     setSSolver (mk_solver "safe" safe_solver)
     setSolver (mk_solver "unsafe" unsafe_solver)
-    setmksimps (map mk_meta_eq o atomize o gen_all)
+    setmksimps (K (map mk_meta_eq o atomize o gen_all))
     setmkcong mk_meta_cong;
 
 val LK_simps =
diff -r 7cb6b40d19b2 -r 0e7fc5bf38de src/ZF/Main_ZF.thy
--- a/src/ZF/Main_ZF.thy	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/ZF/Main_ZF.thy	Thu Apr 29 22:56:32 2010 +0200
@@ -71,7 +71,7 @@
 
 
 declaration {* fn _ =>
-  Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
+  Simplifier.map_ss (fn ss => ss setmksimps (K (map mk_eq o Ord_atomize o gen_all)))
 *}
 
 end
diff -r 7cb6b40d19b2 -r 0e7fc5bf38de src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/ZF/OrdQuant.thy	Thu Apr 29 22:56:32 2010 +0200
@@ -363,7 +363,7 @@
              ZF_mem_pairs);
 *}
 declaration {* fn _ =>
-  Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
+  Simplifier.map_ss (fn ss => ss setmksimps (K (map mk_eq o Ord_atomize o gen_all)))
 *}
 
 text {* Setting up the one-point-rule simproc *}
diff -r 7cb6b40d19b2 -r 0e7fc5bf38de src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -328,7 +328,7 @@
      (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
        If the premises get simplified, then the proofs could fail.*)
      val min_ss = Simplifier.global_context thy empty_ss
-           setmksimps (map mk_eq o ZF_atomize o gen_all)
+           setmksimps (K (map mk_eq o ZF_atomize o gen_all))
            setSolver (mk_solver "minimal"
                       (fn prems => resolve_tac (triv_rls@prems)
                                    ORELSE' assume_tac
diff -r 7cb6b40d19b2 -r 0e7fc5bf38de src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/ZF/simpdata.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -44,7 +44,7 @@
 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
 
 change_simpset (fn ss =>
-  ss setmksimps (map mk_eq o ZF_atomize o gen_all)
+  ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
   addcongs [@{thm if_weak_cong}]);
 
 local