# HG changeset patch
# User wenzelm
# Date 1129651165 -7200
# Node ID 62c397c17d18a170a0f12eb5d2086062eaef2b74
# Parent  7a6c4d60a9130e5e166acaae08e7c462ee220063
Simplifier.theory_context;

diff -r 7a6c4d60a913 -r 62c397c17d18 TFL/rules.ML
--- a/TFL/rules.ML	Tue Oct 18 17:59:24 2005 +0200
+++ b/TFL/rules.ML	Tue Oct 18 17:59:25 2005 +0200
@@ -664,7 +664,8 @@
 
 fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
  let val globals = func::G
-     val pbeta_reduce = simpl_conv empty_ss [split_conv RS eq_reflection];
+     val ss0 = Simplifier.theory_context (Thm.theory_of_thm th) empty_ss
+     val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection];
      val tc_list = ref[]: term list ref
      val dummy = term_ref := []
      val dummy = thm_ref  := []
@@ -805,7 +806,7 @@
     val ctm = cprop_of th
     val names = add_term_names (term_of ctm, [])
     val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
-      (prover names) (empty_ss addsimps [cut_lemma'] addeqcongs congs) ctm
+      (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
     val th2 = equal_elim th1 th
  in
  (th2, List.filter (not o restricted) (!tc_list))
diff -r 7a6c4d60a913 -r 62c397c17d18 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Tue Oct 18 17:59:24 2005 +0200
+++ b/src/FOL/simpdata.ML	Tue Oct 18 17:59:25 2005 +0200
@@ -330,7 +330,8 @@
                                  eq_assume_tac, ematch_tac [FalseE]];
 
 (*No simprules, but basic infastructure for simplification*)
-val FOL_basic_ss = empty_ss
+val FOL_basic_ss =
+  Simplifier.theory_context (the_context ()) empty_ss
   setsubgoaler asm_simp_tac
   setSSolver (mk_solver "FOL safe" safe_solver)
   setSolver (mk_solver "FOL unsafe" unsafe_solver)
diff -r 7a6c4d60a913 -r 62c397c17d18 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Tue Oct 18 17:59:24 2005 +0200
+++ b/src/HOL/Import/shuffler.ML	Tue Oct 18 17:59:25 2005 +0200
@@ -490,8 +490,9 @@
 	val sg = sign_of thy
 
 	val norms = ShuffleData.get thy
-	val ss = empty_ss setmksimps single
-			  addsimps (map (Thm.transfer sg) norms)
+	val ss = Simplifier.theory_context thy empty_ss
+          setmksimps single
+	  addsimps (map (Thm.transfer sg) norms)
 	fun chain f th =
 	    let
                 val rhs = snd (dest_equals (cprop_of th))
diff -r 7a6c4d60a913 -r 62c397c17d18 src/HOL/Prolog/HOHH.ML
--- a/src/HOL/Prolog/HOHH.ML	Tue Oct 18 17:59:24 2005 +0200
+++ b/src/HOL/Prolog/HOHH.ML	Tue Oct 18 17:59:25 2005 +0200
@@ -54,7 +54,10 @@
     | _                             => [thm]
 in map zero_var_indexes (at thm) end;
 
-val atomize_ss = empty_ss setmksimps (mksimps mksimps_pairs) addsimps [
+val atomize_ss =
+  Simplifier.theory_context (the_context ()) empty_ss
+  setmksimps (mksimps mksimps_pairs)
+  addsimps [
         all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
         imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
         imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
diff -r 7a6c4d60a913 -r 62c397c17d18 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Oct 18 17:59:24 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue Oct 18 17:59:25 2005 +0200
@@ -317,7 +317,7 @@
 
 val is_selector = Symtab.defined o #selectors o get_sel_upd;
 val get_updates = Symtab.lookup o #updates o get_sel_upd;
-val get_simpset = #simpset o get_sel_upd;
+fun get_simpset thy = Simplifier.theory_context thy (#simpset (get_sel_upd thy));
 
 fun put_sel_upd names simps thy =
   let
@@ -1119,8 +1119,6 @@
 fun record_split_simp_tac thms P i st =
   let
     val sg = Thm.sign_of_thm st;
-    val {sel_upd={simpset,...},...}
-            = RecordsData.get sg;
 
     val has_rec = exists_Const
       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
@@ -1158,7 +1156,7 @@
     val simprocs = if has_rec goal then [record_split_simproc P] else [];
 
   in st |> ((EVERY split_frees_tacs)
-           THEN (Simplifier.full_simp_tac (simpset addsimps thms addsimprocs simprocs) i))
+           THEN (Simplifier.full_simp_tac (get_simpset sg addsimps thms addsimprocs simprocs) i))
   end handle Empty => Seq.empty;
 end;
 
diff -r 7a6c4d60a913 -r 62c397c17d18 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Oct 18 17:59:24 2005 +0200
+++ b/src/HOL/simpdata.ML	Tue Oct 18 17:59:25 2005 +0200
@@ -341,7 +341,8 @@
 val safe_solver = mk_solver "HOL safe" safe_solver_tac;
 
 val HOL_basic_ss =
-  empty_ss setsubgoaler asm_simp_tac
+  Simplifier.theory_context (the_context ()) empty_ss
+    setsubgoaler asm_simp_tac
     setSSolver safe_solver
     setSolver unsafe_solver
     setmksimps (mksimps mksimps_pairs)
@@ -460,14 +461,13 @@
 *)
 
 local
-  val nnf_simps =
-        [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj,
-         not_all,not_ex,not_not];
   val nnf_simpset =
-        empty_ss setmkeqTrue mk_eq_True
-                 setmksimps (mksimps mksimps_pairs)
-                 addsimps nnf_simps;
-  val prem_nnf_tac = full_simp_tac nnf_simpset
+    empty_ss setmkeqTrue mk_eq_True
+    setmksimps (mksimps mksimps_pairs)
+    addsimps [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj,
+      not_all,not_ex,not_not];
+  fun prem_nnf_tac i st =
+    full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st;
 in
 fun refute_tac test prep_tac ref_tac =
   let val refute_prems_tac =
diff -r 7a6c4d60a913 -r 62c397c17d18 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Tue Oct 18 17:59:24 2005 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Oct 18 17:59:25 2005 +0200
@@ -79,7 +79,7 @@
   val trace           : bool ref
   val fast_arith_neq_limit: int ref
   val lin_arith_prover: theory -> simpset -> term -> thm option
-  val     lin_arith_tac:     bool -> int -> tactic
+  val     lin_arith_tac:    bool -> int -> tactic
   val cut_lin_arith_tac: simpset -> int -> tactic
 end;
 
@@ -665,7 +665,9 @@
      | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i,js))
   end) i st;
 
-val lin_arith_tac = simpset_lin_arith_tac Simplifier.empty_ss;
+fun lin_arith_tac ex i st =
+  simpset_lin_arith_tac (Simplifier.theory_context (Thm.theory_of_thm st) Simplifier.empty_ss)
+    ex i st;
 
 fun cut_lin_arith_tac ss i =
   cut_facts_tac (Simplifier.prems_of_ss ss) i THEN
diff -r 7a6c4d60a913 -r 62c397c17d18 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Tue Oct 18 17:59:24 2005 +0200
+++ b/src/Pure/tactic.ML	Tue Oct 18 17:59:25 2005 +0200
@@ -535,8 +535,10 @@
 val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
 
 fun rewrite_goal_tac rews =
-  MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac)
-    (MetaSimplifier.empty_ss addsimps rews);
+  let val ss = MetaSimplifier.empty_ss addsimps rews in
+    fn i => fn st => MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac)
+      (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
+  end;
 
 (*Rewrite throughout proof state. *)
 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
diff -r 7a6c4d60a913 -r 62c397c17d18 src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Tue Oct 18 17:59:24 2005 +0200
+++ b/src/Sequents/simpdata.ML	Tue Oct 18 17:59:25 2005 +0200
@@ -235,7 +235,8 @@
 
 (*No simprules, but basic infrastructure for simplification*)
 val LK_basic_ss =
-  empty_ss setsubgoaler asm_simp_tac
+  Simplifier.theory_context (the_context ()) empty_ss
+    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)
diff -r 7a6c4d60a913 -r 62c397c17d18 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Tue Oct 18 17:59:24 2005 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Tue Oct 18 17:59:25 2005 +0200
@@ -339,7 +339,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 = empty_ss
+     val min_ss = Simplifier.theory_context thy empty_ss
            setmksimps (map mk_eq o ZF_atomize o gen_all)
            setSolver (mk_solver "minimal"
                       (fn prems => resolve_tac (triv_rls@prems)