# HG changeset patch
# User wenzelm
# Date 1129583410 -7200
# Node ID d810945150611b585a08813bb2bd49054647ed4b
# Parent  8be65cf94d2e103cb8a3b0d4e6aabc23fd2b1d84
change_claset/simpset;
Simplifier.inherit_context instead of Simplifier.inherit_bounds;

diff -r 8be65cf94d2e -r d81094515061 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Mon Oct 17 19:19:29 2005 +0200
+++ b/src/FOL/simpdata.ML	Mon Oct 17 23:10:10 2005 +0200
@@ -339,7 +339,7 @@
 
 fun unfold_tac ss ths =
   ALLGOALS (full_simp_tac
-    (Simplifier.inherit_bounds ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
+    (Simplifier.inherit_context ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
 
 
 (*intuitionistic simprules only*)
@@ -360,7 +360,7 @@
 (*classical simprules too*)
 val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
 
-val simpsetup = [fn thy => (simpset_ref_of thy := FOL_ss; thy)];
+val simpsetup = [fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy)];
 
 
 (*** integration of simplifier with classical reasoner ***)
diff -r 8be65cf94d2e -r d81094515061 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Mon Oct 17 19:19:29 2005 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Mon Oct 17 23:10:10 2005 +0200
@@ -309,7 +309,7 @@
   | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
 
 fun simplify_meta_eq rules ss =
-    simplify (Simplifier.inherit_bounds ss HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
+    simplify (Simplifier.inherit_context ss HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
     o mk_meta_eq;
 
 structure CancelNumeralsCommon =
@@ -321,14 +321,14 @@
   val find_first_coeff  = find_first_coeff []
   val trans_tac         = fn _ => trans_tac
   fun norm_tac ss =
-    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
+    let val num_ss' = Simplifier.inherit_context ss num_ss in
       ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
                                          diff_simps @ minus_simps @ add_ac))
       THEN ALLGOALS (simp_tac (num_ss' addsimps non_add_bin_simps @ mult_minus_simps))
       THEN ALLGOALS (simp_tac (num_ss' addsimps minus_from_mult_simps @ add_ac @ mult_ac))
     end
   fun numeral_simp_tac ss =
-    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
+    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
   val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
   end;
 
@@ -399,14 +399,14 @@
   val prove_conv        = Bin_Simprocs.prove_conv_nohyps
   val trans_tac         = fn _ => trans_tac
   fun norm_tac ss =
-    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
+    let val num_ss' = Simplifier.inherit_context ss num_ss in
       ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
                                           diff_simps @ minus_simps @ add_ac))
       THEN ALLGOALS (simp_tac (num_ss' addsimps non_add_bin_simps @ mult_minus_simps))
       THEN ALLGOALS (simp_tac (num_ss' addsimps minus_from_mult_simps @ add_ac @ mult_ac))
     end
   fun numeral_simp_tac ss =
-    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
+    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
   val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
   end;
 
diff -r 8be65cf94d2e -r d81094515061 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Oct 17 19:19:29 2005 +0200
+++ b/src/HOL/Product_Type.thy	Mon Oct 17 23:10:10 2005 +0200
@@ -320,7 +320,7 @@
    if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th;
   end;
 
-claset_ref() := claset() addSbefore ("split_all_tac", split_all_tac);
+change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
 *}
 
 lemma split_paired_All [simp]: "(ALL x. P x) = (ALL a b. P (a, b))"
@@ -415,7 +415,7 @@
   |   split_pat tp i _ = NONE;
   fun metaeq thy ss lhs rhs = mk_meta_eq (Tactic.prove thy [] []
         (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
-        (K (simp_tac (Simplifier.inherit_bounds ss HOL_basic_ss addsimps [cond_split_eta]) 1)));
+        (K (simp_tac (Simplifier.inherit_context ss HOL_basic_ss addsimps [cond_split_eta]) 1)));
 
   fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
   |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
@@ -529,7 +529,7 @@
 end;
 (* This prevents applications of splitE for already splitted arguments leading
    to quite time-consuming computations (in particular for nested tuples) *)
-claset_ref() := claset() addSbefore ("split_conv_tac", split_conv_tac);
+change_claset (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac));
 *}
 
 lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
diff -r 8be65cf94d2e -r d81094515061 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Oct 17 19:19:29 2005 +0200
+++ b/src/HOL/Set.thy	Mon Oct 17 23:10:10 2005 +0200
@@ -380,7 +380,7 @@
 *}
 
 ML_setup {*
-  claset_ref() := claset() addbefore ("bspec", datac (thm "bspec") 1);
+  change_claset (fn cs => cs addbefore ("bspec", datac (thm "bspec") 1));
 *}
 
 lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
@@ -431,7 +431,7 @@
 
     val simpset = Simplifier.clear_ss HOL_basic_ss;
     fun unfold_tac ss th =
-      ALLGOALS (full_simp_tac (Simplifier.inherit_bounds ss simpset addsimps [th]));
+      ALLGOALS (full_simp_tac (Simplifier.inherit_context ss simpset addsimps [th]));
 
     fun prove_bex_tac ss =
       unfold_tac ss Bex_def THEN Quantifier1.prove_one_point_ex_tac;
@@ -977,7 +977,7 @@
 
 ML_setup {*
   val mksimps_pairs = [("Ball", [thm "bspec"])] @ mksimps_pairs;
-  simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs);
+  change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
 *}
 
 declare subset_UNIV [simp] subset_refl [simp]
diff -r 8be65cf94d2e -r d81094515061 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Oct 17 19:19:29 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Mon Oct 17 23:10:10 2005 +0200
@@ -352,7 +352,7 @@
                                     atac 2, resolve_tac thms 1, etac FalseE 1])))
                                | ManyConstrs (thm, simpset) => SOME (Tactic.prove sg [] [] eq_t (K
                                    (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
-                                    full_simp_tac (Simplifier.inherit_bounds ss simpset) 1,
+                                    full_simp_tac (Simplifier.inherit_context ss simpset) 1,
                                     REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
                                     eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
                                     etac FalseE 1]))))
@@ -372,7 +372,7 @@
 
 val simproc_setup =
   [Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t),
-   fn thy => (simpset_ref_of thy := simpset_of thy addsimprocs [distinct_simproc]; thy)];
+   fn thy => ((change_simpset_of thy) (fn ss => ss addsimprocs [distinct_simproc]); thy)];
 
 
 (**** translation rules for case ****)
diff -r 8be65cf94d2e -r d81094515061 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Mon Oct 17 19:19:29 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Mon Oct 17 23:10:10 2005 +0200
@@ -826,7 +826,7 @@
                  | NONE => extsplits)
   in
     quick_and_dirty_prove true sg [] prop
-      (fn _ => simp_tac (Simplifier.inherit_bounds ss simpset addsimps thms) 1)
+      (fn _ => simp_tac (Simplifier.inherit_context ss simpset addsimps thms) 1)
   end;
 
 
@@ -1069,7 +1069,7 @@
        let
          fun prove prop =
            quick_and_dirty_prove true sg [] prop
-             (fn _ => simp_tac (Simplifier.inherit_bounds ss (get_simpset sg)
+             (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset sg)
                addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1);
 
          fun mkeq (lr,Teq,(sel,Tsel),x) i =
@@ -2106,8 +2106,8 @@
  [RecordsData.init,
   Theory.add_trfuns ([], parse_translation, [], []),
   Theory.add_advanced_trfuns ([], adv_parse_translation, [], []),
-  Simplifier.change_simpset_of Simplifier.addsimprocs
-    [record_simproc, record_upd_simproc, record_eq_simproc]];
+  (fn thy => (Simplifier.change_simpset_of thy
+    (fn ss => ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); thy))];
 
 (* outer syntax *)
 
diff -r 8be65cf94d2e -r d81094515061 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Mon Oct 17 19:19:29 2005 +0200
+++ b/src/HOL/arith_data.ML	Mon Oct 17 23:10:10 2005 +0200
@@ -64,7 +64,7 @@
 (* rewriting *)
 
 fun simp_all_tac rules ss =
-  ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps rules));
+  ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps rules));
 
 val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
 val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
@@ -394,7 +394,7 @@
 val add_rules =
  [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
   One_nat_def,isolateSuc,
-  order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one, 
+  order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one,
   zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero];
 
 val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s
@@ -431,7 +431,7 @@
     neqE = [linorder_neqE_nat,
       get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")],
     simpset = HOL_basic_ss addsimps add_rules
-                   addsimprocs [ab_group_add_cancel.sum_conv, 
+                   addsimprocs [ab_group_add_cancel.sum_conv,
                                 ab_group_add_cancel.rel_conv]
                    (*abel_cancel helps it work in abstract algebraic domains*)
                    addsimprocs nat_cancel_sums_add}),
@@ -538,15 +538,14 @@
 (* theory setup *)
 
 val arith_setup =
- [Simplifier.change_simpset_of (op addsimprocs) nat_cancel_sums] @
   init_lin_arith_data @
-  [Simplifier.change_simpset_of (op addSolver)
-   (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac),
-  Simplifier.change_simpset_of (op addsimprocs) [fast_nat_arith_simproc],
+  [fn thy => (Simplifier.change_simpset_of thy (fn ss => ss
+    addsimprocs (nat_cancel_sums @ [fast_nat_arith_simproc])
+    addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy),
   Method.add_methods
-      [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
-	"decide linear arithmethic")],
+    [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
+      "decide linear arithmethic")],
   Attrib.add_attributes [("arith_split",
-    (Attrib.no_args arith_split_add, 
+    (Attrib.no_args arith_split_add,
      Attrib.no_args Attrib.undef_local_attribute),
     "declaration of split rules for arithmetic procedure")]];
diff -r 8be65cf94d2e -r d81094515061 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Mon Oct 17 19:19:29 2005 +0200
+++ b/src/HOL/simpdata.ML	Mon Oct 17 23:10:10 2005 +0200
@@ -350,7 +350,7 @@
 
 fun unfold_tac ss ths =
   ALLGOALS (full_simp_tac
-    (Simplifier.inherit_bounds ss (Simplifier.clear_ss HOL_basic_ss) addsimps ths));
+    (Simplifier.inherit_context ss (Simplifier.clear_ss HOL_basic_ss) addsimps ths));
 
 (*In general it seems wrong to add distributive laws by default: they
   might cause exponential blow-up.  But imp_disjL has been in for a while
@@ -424,7 +424,7 @@
 
 (* default simpset *)
 val simpsetup =
-  [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)];
+  [fn thy => (change_simpset_of thy (fn _ => HOL_ss addcongs [if_weak_cong]); thy)];
 
 
 (*** integration of simplifier with classical reasoner ***)