# HG changeset patch
# User wenzelm
# Date 1122916826 -7200
# Node ID b2a894562b8fdc9544e1df035349cf46e7017eeb
# Parent  d3f9abe007124ba7e89597dd9edd6cd4bf366de6
simprocs: Simplifier.inherit_bounds;

diff -r d3f9abe00712 -r b2a894562b8f src/HOL/Algebra/abstract/Ring.thy
--- a/src/HOL/Algebra/abstract/Ring.thy	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Algebra/abstract/Ring.thy	Mon Aug 01 19:20:26 2005 +0200
@@ -163,11 +163,11 @@
 	 "t - u::'a::ring",
 	 "t * u::'a::ring",
 	 "- t::'a::ring"];
-    fun proc sg _ t = 
+    fun proc sg ss t = 
       let val rew = Tactic.prove sg [] []
             (HOLogic.mk_Trueprop
               (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
-                (fn _ => simp_tac ring_ss 1)
+                (fn _ => simp_tac (Simplifier.inherit_bounds ss ring_ss) 1)
             |> mk_meta_eq;
           val (t', u) = Logic.dest_equals (Thm.prop_of rew);
       in if t' aconv u 
@@ -175,7 +175,7 @@
         else SOME rew 
     end;
   in
-    val ring_simproc = Simplifier.simproc (sign_of (the_context ())) "ring" lhss proc;
+    val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss proc;
   end;
 *}
 
diff -r d3f9abe00712 -r b2a894562b8f src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Fun.thy	Mon Aug 01 19:20:26 2005 +0200
@@ -486,15 +486,18 @@
         | find t = NONE
     in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
 
-  val ss = simpset ()
-  val fun_upd_prover = K (rtac eq_reflection 1 THEN rtac ext 1 THEN simp_tac ss 1)
+  val current_ss = simpset ()
+  fun fun_upd_prover ss =
+    rtac eq_reflection 1 THEN rtac ext 1 THEN
+    simp_tac (Simplifier.inherit_bounds ss current_ss) 1
 in
   val fun_upd2_simproc =
     Simplifier.simproc (Theory.sign_of (the_context ()))
       "fun_upd2" ["f(v := w, x := y)"]
-      (fn sg => fn _ => fn t =>
+      (fn sg => fn ss => fn t =>
         case find_double t of (T, NONE) => NONE
-        | (T, SOME rhs) => SOME (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) fun_upd_prover))
+        | (T, SOME rhs) =>
+            SOME (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
 end;
 Addsimprocs[fun_upd2_simproc];
 
diff -r d3f9abe00712 -r b2a894562b8f src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Mon Aug 01 19:20:26 2005 +0200
@@ -150,7 +150,7 @@
   ordering is not well-founded.*)
 fun num_ord (i,j) =
       (case IntInf.compare (IntInf.abs i, IntInf.abs j) of
-            EQUAL => Int.compare (IntInf.sign i, IntInf.sign j) 
+            EQUAL => int_ord (IntInf.sign i, IntInf.sign j) 
           | ord => ord);
 
 (*This resembles Term.term_ord, but it puts binary numerals before other
@@ -165,7 +165,7 @@
   | numterm_ord (Const("Numeral.number_of", _) $ _, _) = LESS
   | numterm_ord (_, Const("Numeral.number_of", _) $ _) = GREATER
   | numterm_ord (t, u) =
-      (case Int.compare (size_of_term t, size_of_term u) of
+      (case int_ord (size_of_term t, size_of_term u) of
         EQUAL =>
           let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
             (case hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
@@ -308,8 +308,8 @@
 fun trans_tac NONE      = all_tac
   | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
 
-fun simplify_meta_eq rules =
-    simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
+fun simplify_meta_eq rules ss =
+    simplify (Simplifier.inherit_bounds ss HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
     o mk_meta_eq;
 
 structure CancelNumeralsCommon =
@@ -319,15 +319,17 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff 1
   val find_first_coeff  = find_first_coeff []
-  val trans_tac         = trans_tac
-  val norm_tac =
-     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))
-  val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
-  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
+  val trans_tac         = fn _ => trans_tac
+  fun norm_tac ss =
+    let val num_ss' = Simplifier.inherit_bounds 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))
+  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
   end;
 
 
@@ -395,16 +397,17 @@
   val dest_coeff        = dest_coeff 1
   val left_distrib      = combine_common_factor RS trans
   val prove_conv        = Bin_Simprocs.prove_conv_nohyps
-  val trans_tac          = trans_tac
-  val norm_tac =
-     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))
-  val numeral_simp_tac  = ALLGOALS
-                    (simp_tac (HOL_ss addsimps add_0s@bin_simps))
-  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
+  val trans_tac         = fn _ => trans_tac
+  fun norm_tac ss =
+    let val num_ss' = Simplifier.inherit_bounds 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))
+  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
   end;
 
 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
diff -r d3f9abe00712 -r b2a894562b8f src/HOL/Integ/int_factor_simprocs.ML
--- a/src/HOL/Integ/int_factor_simprocs.ML	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML	Mon Aug 01 19:20:26 2005 +0200
@@ -42,14 +42,16 @@
   struct
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff 1
-  val trans_tac         = trans_tac
-  val norm_tac =
-     ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps @ mult_1s))
-     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_minus_simps))
-     THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
-  val numeral_simp_tac  =
-         ALLGOALS (simp_tac (HOL_ss addsimps rel_number_of@bin_simps))
-  val simplify_meta_eq  = 
+  val trans_tac         = fn _ => trans_tac
+  fun norm_tac ss =
+    let val HOL_ss' = Simplifier.inherit_bounds ss HOL_ss in
+      ALLGOALS (simp_tac (HOL_ss' addsimps minus_from_mult_simps @ mult_1s))
+      THEN ALLGOALS (simp_tac (HOL_ss' addsimps bin_simps@mult_minus_simps))
+      THEN ALLGOALS (simp_tac (HOL_ss' addsimps mult_ac))
+    end
+  fun numeral_simp_tac ss =
+    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps rel_number_of @ bin_simps))
+  val simplify_meta_eq = 
 	Int_Numeral_Simprocs.simplify_meta_eq
 	     [add_0, add_0_right,
 	      mult_zero_left, mult_zero_right, mult_1, mult_1_right];
@@ -235,8 +237,8 @@
     Int_Numeral_Simprocs.simplify_meta_eq  
        [mult_1_left, mult_1_right, zdiv_1, numeral_1_eq_1];
 
-fun cancel_simplify_meta_eq cancel_th th =
-    simplify_one (([th, cancel_th]) MRS trans);
+fun cancel_simplify_meta_eq cancel_th ss th =
+    simplify_one ss (([th, cancel_th]) MRS trans);
 
 (*At present, long_mk_prod creates Numeral1, so this requires the axclass
   number_ring*)
@@ -247,8 +249,9 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val find_first        = find_first []
-  val trans_tac         = trans_tac
-  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
+  val trans_tac         = fn _ => trans_tac
+  fun norm_tac ss =
+    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps mult_1s @ mult_ac))
   end;
 
 (*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in
diff -r d3f9abe00712 -r b2a894562b8f src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Mon Aug 01 19:20:26 2005 +0200
@@ -168,14 +168,15 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val find_first_coeff  = find_first_coeff []
-  val trans_tac          = trans_tac
-  val norm_tac = ALLGOALS
-                   (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
+  val trans_tac         = fn _ => trans_tac
+  fun norm_tac ss =
+    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
+      ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
                                 [Suc_eq_add_numeral_1_left] @ add_ac))
-                 THEN ALLGOALS (simp_tac
-                                (num_ss addsimps bin_simps@add_ac@mult_ac))
-  val numeral_simp_tac  = ALLGOALS
-                (simp_tac (HOL_ss addsimps add_0s@bin_simps))
+      THEN ALLGOALS (simp_tac (num_ss' addsimps bin_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))
   val simplify_meta_eq  = simplify_meta_eq
   end;
 
@@ -252,14 +253,15 @@
   val dest_coeff        = dest_coeff
   val left_distrib      = left_add_mult_distrib RS trans
   val prove_conv        = Bin_Simprocs.prove_conv_nohyps
-  val trans_tac          = trans_tac
-  val norm_tac = ALLGOALS
-                   (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
+  val trans_tac         = fn _ => trans_tac
+  fun norm_tac ss =
+    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
+      ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
                               [Suc_eq_add_numeral_1] @ add_ac))
-                 THEN ALLGOALS (simp_tac
-                                (num_ss addsimps bin_simps@add_ac@mult_ac))
-  val numeral_simp_tac  = ALLGOALS
-                (simp_tac (HOL_ss addsimps add_0s@bin_simps))
+      THEN ALLGOALS (simp_tac (num_ss' addsimps bin_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))
   val simplify_meta_eq  = simplify_meta_eq
   end;
 
@@ -275,13 +277,15 @@
   struct
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
-  val trans_tac         = trans_tac
-  val norm_tac = ALLGOALS
-                   (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
+  val trans_tac         = fn _ => trans_tac
+  fun norm_tac ss =
+    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
+      ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
                                 [Suc_eq_add_numeral_1_left] @ add_ac))
-                 THEN ALLGOALS (simp_tac
-                                (num_ss addsimps bin_simps@add_ac@mult_ac))
-  val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
+      THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac))
+    end
+  fun numeral_simp_tac ss =
+    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps bin_simps))
   val simplify_meta_eq  = simplify_meta_eq
   end
 
@@ -356,8 +360,8 @@
     Int_Numeral_Simprocs.simplify_meta_eq  
        [mult_1_left, mult_1_right, div_1, numeral_1_eq_Suc_0];
 
-fun cancel_simplify_meta_eq cancel_th th =
-    simplify_one (([th, cancel_th]) MRS trans);
+fun cancel_simplify_meta_eq cancel_th ss th =
+    simplify_one ss (([th, cancel_th]) MRS trans);
 
 structure CancelFactorCommon =
   struct
@@ -366,8 +370,9 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val find_first        = find_first []
-  val trans_tac         = trans_tac
-  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
+  val trans_tac         = fn _ => trans_tac
+  fun norm_tac ss =
+    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps mult_1s @ mult_ac))
   end;
 
 structure EqCancelFactor = ExtractCommonTermFun
diff -r d3f9abe00712 -r b2a894562b8f src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/List.thy	Mon Aug 01 19:20:26 2005 +0200
@@ -415,10 +415,9 @@
   | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
   | butlast xs = Const("List.list.Nil",fastype_of xs);
 
-val rearr_tac =
-  simp_tac (HOL_basic_ss addsimps [append_assoc, append_Nil, append_Cons]);
-
-fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
+val rearr_ss = HOL_basic_ss addsimps [append_assoc, append_Nil, append_Cons];
+
+fun list_eq sg ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
   let
     val lastl = last lhs and lastr = last rhs;
     fun rearr conv =
@@ -429,7 +428,8 @@
         val app = Const("List.op @",appT)
         val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
         val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
-        val thm = Tactic.prove sg [] [] eq (K (rearr_tac 1));
+        val thm = Tactic.prove sg [] [] eq
+          (K (simp_tac (Simplifier.inherit_bounds ss rearr_ss) 1));
       in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
 
   in
diff -r d3f9abe00712 -r b2a894562b8f src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Real/RealDef.thy	Mon Aug 01 19:20:26 2005 +0200
@@ -425,9 +425,9 @@
                  linorder_not_le [where 'a = preal] 
                   real_zero_def real_le real_mult)
   --{*Reduce to the (simpler) @{text "\<le>"} relation *}
-apply (auto  dest!: less_add_left_Ex 
+apply (auto dest!: less_add_left_Ex
      simp add: preal_add_ac preal_mult_ac 
-          preal_add_mult_distrib2 preal_cancels preal_self_less_add_right)
+          preal_add_mult_distrib2 preal_cancels preal_self_less_add_left)
 done
 
 lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y"
@@ -478,7 +478,6 @@
 apply (auto simp add: real_minus preal_add_ac)
 apply (cut_tac x = x and y = y in linorder_less_linear)
 apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc [symmetric])
-apply (auto simp add: preal_add_commute)
 done
 
 lemma real_of_preal_leD:
diff -r d3f9abe00712 -r b2a894562b8f src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Mon Aug 01 19:20:26 2005 +0200
@@ -326,7 +326,7 @@
 
 exception ConstrDistinct of term;
 
-fun distinct_proc sg _ (t as Const ("op =", _) $ t1 $ t2) =
+fun distinct_proc sg ss (t as Const ("op =", _) $ t1 $ t2) =
   (case (stripC (0, t1), stripC (0, t2)) of
      ((i, Const (cname1, T1)), (j, Const (cname2, T2))) =>
          (case (stripT (0, T1), stripT (0, T2)) of
@@ -347,9 +347,9 @@
                                | FewConstrs thms => SOME (Tactic.prove sg [] [] eq_t (K
                                    (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
                                     atac 2, resolve_tac thms 1, etac FalseE 1])))
-                               | ManyConstrs (thm, ss) => SOME (Tactic.prove sg [] [] eq_t (K
+                               | ManyConstrs (thm, simpset) => SOME (Tactic.prove sg [] [] eq_t (K
                                    (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
-                                    full_simp_tac ss 1,
+                                    full_simp_tac (Simplifier.inherit_bounds 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]))))
diff -r d3f9abe00712 -r b2a894562b8f src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Mon Aug 01 19:20:26 2005 +0200
@@ -833,7 +833,7 @@
       else opt ();
 
 
-fun prove_split_simp sg T prop =
+fun prove_split_simp sg ss T prop =
   let 
     val {sel_upd={simpset,...},extsplit,...} = RecordsData.get sg;
     val extsplits = 
@@ -844,7 +844,9 @@
                      all_thm::(case extsplits of [thm] => [] | _ => extsplits)
                               (* [thm] is the same as all_thm *)
                  | NONE => extsplits)                                
-  in (quick_and_dirty_prove true sg [] prop (fn _ => (simp_tac (simpset addsimps thms) 1)))
+  in
+    quick_and_dirty_prove true sg [] prop
+      (fn _ => simp_tac (Simplifier.inherit_bounds ss simpset addsimps thms) 1)
   end;
 
 
@@ -868,7 +870,7 @@
  *)
 val record_simproc =
   Simplifier.simproc (Theory.sign_of HOL.thy) "record_simp" ["s (u k r)"]
-    (fn sg => fn _ => fn t =>
+    (fn sg => fn ss => fn t =>
       (case t of (sel as Const (s, Type (_,[domS,rangeS])))$
                    ((upd as Const (u,Type(_,[_,Type (_,[rT,_])]))) $ k $ r)=>
         (case get_selectors sg s of SOME () =>
@@ -908,9 +910,9 @@
 	      (case mk_eq_terms (upd$k$r) of
                  SOME (trm,trm',vars,update_s) 
                  => if update_s 
-		    then SOME (prove_split_simp sg domS 
+		    then SOME (prove_split_simp sg ss domS 
                                  (list_all(vars,(equals rangeS$(sel$trm)$trm'))))
-                    else SOME (prove_split_simp sg domS 
+                    else SOME (prove_split_simp sg ss domS 
                                  (list_all(vars,(equals rangeS$(sel$trm)$(sel$trm')))))
                | NONE => NONE)
             end
@@ -929,7 +931,7 @@
 *)
 val record_upd_simproc =
   Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u k r)"]
-    (fn sg => fn _ => fn t =>
+    (fn sg => fn ss => fn t =>
       (case t of ((upd as Const (u, Type(_,[_,Type(_,[rT,_])]))) $ k $ r) =>
  	 let datatype ('a,'b) calc = Init of 'b | Inter of 'a  
              val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get sg;
@@ -1020,7 +1022,7 @@
 
 	 in (case mk_updterm updates [] t of
 	       Inter (trm,trm',vars,_)
-                => SOME (prove_split_simp sg rT  
+                => SOME (prove_split_simp sg ss rT  
                           (list_all(vars,(equals rT$trm$trm'))))
              | _ => NONE)
 	 end
@@ -1083,11 +1085,12 @@
 
 val record_ex_sel_eq_simproc =
   Simplifier.simproc (Theory.sign_of HOL.thy) "record_ex_sel_eq_simproc" ["Ex t"]
-    (fn sg => fn _ => fn t =>
+    (fn sg => fn ss => fn t =>
        let 
-         fun prove prop = (quick_and_dirty_prove true sg [] prop 
-                             (fn _ => (simp_tac ((get_simpset sg) addsimps simp_thms
-                                        addsimprocs [record_split_simproc (K ~1)]) 1)));
+         fun prove prop =
+           quick_and_dirty_prove true sg [] prop
+             (fn _ => simp_tac (Simplifier.inherit_bounds ss (get_simpset sg)
+               addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1);
 
          fun mkeq (lr,Teq,(sel,Tsel),x) i =
               (case get_selectors sg sel of SOME () =>
diff -r d3f9abe00712 -r b2a894562b8f src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Mon Aug 01 19:20:26 2005 +0200
@@ -88,10 +88,10 @@
 
 (* A simproc to cancel complementary terms in arbitrary sums. *)
 
-fun sum_proc sg _ t =
+fun sum_proc sg ss t =
    let val t' = cancel sg t
        val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
-                   (fn _ => simp_tac cancel_ss 1)
+                   (fn _ => simp_tac (Simplifier.inherit_bounds ss cancel_ss) 1)
    in SOME thm end
    handle Cancel => NONE;
 
@@ -108,12 +108,12 @@
    Reduces the problem to subtraction.
  *)
 
- fun rel_proc sg _ t =
+ fun rel_proc sg ss t =
    let val t' = cancel sg t
        val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
                    (fn _ => rtac eq_reflection 1 THEN
                             resolve_tac eqI_rules 1 THEN
-                            simp_tac cancel_ss 1)
+                            simp_tac (Simplifier.inherit_bounds ss cancel_ss) 1)
    in SOME thm end
    handle Cancel => NONE;
 
diff -r d3f9abe00712 -r b2a894562b8f src/Provers/Arith/assoc_fold.ML
--- a/src/Provers/Arith/assoc_fold.ML	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/Provers/Arith/assoc_fold.ML	Mon Aug 01 19:20:26 2005 +0200
@@ -42,7 +42,7 @@
  val trace = ref false;
 
  (*Make a simproc to combine all literals in a associative nest*)
- fun proc thy _ lhs =
+ fun proc thy ss lhs =
    let fun show t = string_of_cterm (Thm.cterm_of thy t)
        val _ = if !trace then tracing ("assoc_fold simproc: LHS = " ^ show lhs)
                else ()
@@ -56,7 +56,7 @@
        val _ = if !trace then tracing ("RHS = " ^ show rhs) else ()
        val th = Tactic.prove thy [] [] (Logic.mk_equals (lhs, rhs))
                    (fn _ => rtac Data.eq_reflection 1 THEN
-                            simp_tac assoc_ss 1)
+                            simp_tac (Simplifier.inherit_bounds ss assoc_ss) 1)
    in SOME th end
    handle Assoc_fail => NONE;
 
diff -r d3f9abe00712 -r b2a894562b8f src/Provers/Arith/cancel_numeral_factor.ML
--- a/src/Provers/Arith/cancel_numeral_factor.ML	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML	Mon Aug 01 19:20:26 2005 +0200
@@ -29,24 +29,24 @@
   val neg_exchanges: bool  (*true if a negative coeff swaps the two operands,
                              as with < and <= but not = and div*)
   (*proof tools*)
-  val prove_conv: tactic list -> Sign.sg -> 
+  val prove_conv: tactic list -> theory -> 
                   thm list -> string list -> term * term -> thm option
-  val trans_tac: thm option -> tactic (*applies the initial lemma*)
-  val norm_tac: tactic                (*proves the initial lemma*)
-  val numeral_simp_tac: tactic        (*proves the final theorem*)
-  val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
+  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
+  val norm_tac: simpset -> tactic                (*proves the initial lemma*)
+  val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
+  val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
 end;
 
 
 functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA):
   sig
-  val proc: Sign.sg -> simpset -> term -> thm option
+  val proc: theory -> simpset -> term -> thm option
   end 
 =
 struct
 
 (*the simplification procedure*)
-fun proc sg ss t =
+fun proc thy ss t =
   let
       val hyps = prems_of_ss ss;
       (*first freeze any Vars in the term to prevent flex-flex problems*)
@@ -67,13 +67,13 @@
                 else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2'))
       val reshape =  (*Move d to the front and put the rest into standard form
 		       i * #m * j == #d * (#n * (j * k)) *)
-	    Data.prove_conv [Data.norm_tac] sg hyps xs
+	    Data.prove_conv [Data.norm_tac ss] thy hyps xs
 	      (t',   Data.mk_bal (newshape(n1,t1'), newshape(n2,t2')))
   in
-      Option.map Data.simplify_meta_eq
+      Option.map (Data.simplify_meta_eq ss)
        (Data.prove_conv 
-	       [Data.trans_tac reshape, rtac Data.cancel 1,
-		Data.numeral_simp_tac] sg hyps xs (t', rhs))
+	       [Data.trans_tac ss reshape, rtac Data.cancel 1,
+		Data.numeral_simp_tac ss] thy hyps xs (t', rhs))
   end
   handle TERM _ => NONE
        | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
diff -r d3f9abe00712 -r b2a894562b8f src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML	Mon Aug 01 19:20:26 2005 +0200
@@ -36,18 +36,18 @@
   val bal_add1: thm
   val bal_add2: thm
   (*proof tools*)
-  val prove_conv: tactic list -> Sign.sg -> 
+  val prove_conv: tactic list -> theory -> 
                   thm list -> string list -> term * term -> thm option
-  val trans_tac: thm option -> tactic (*applies the initial lemma*)
-  val norm_tac: tactic                (*proves the initial lemma*)
-  val numeral_simp_tac: tactic        (*proves the final theorem*)
-  val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
+  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
+  val norm_tac: simpset -> tactic                (*proves the initial lemma*)
+  val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
+  val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
 end;
 
 
 functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
   sig
-  val proc: Sign.sg -> simpset -> term -> thm option
+  val proc: theory -> simpset -> term -> thm option
   end 
 =
 struct
@@ -69,7 +69,7 @@
   in  seek terms1 end;
 
 (*the simplification procedure*)
-fun proc sg ss t =
+fun proc thy ss t =
   let
       val hyps = prems_of_ss ss;
       (*first freeze any Vars in the term to prevent flex-flex problems*)
@@ -86,22 +86,22 @@
 		       i + #m + j + k == #m + i + (j + k) *)
 	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
 		raise TERM("cancel_numerals", []) 
-	    else Data.prove_conv [Data.norm_tac] sg hyps xs
+	    else Data.prove_conv [Data.norm_tac ss] thy hyps xs
 			(t', 
 			 Data.mk_bal (newshape(n1,terms1'), 
 				      newshape(n2,terms2')))
   in
-      Option.map Data.simplify_meta_eq
+      Option.map (Data.simplify_meta_eq ss)
        (if n2<=n1 then 
 	    Data.prove_conv 
-	       [Data.trans_tac reshape, rtac Data.bal_add1 1,
-		Data.numeral_simp_tac] sg hyps xs
+	       [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
+		Data.numeral_simp_tac ss] thy hyps xs
 	       (t', Data.mk_bal (newshape(n1-n2,terms1'), 
 				 Data.mk_sum T terms2'))
 	else
 	    Data.prove_conv 
-	       [Data.trans_tac reshape, rtac Data.bal_add2 1,
-		Data.numeral_simp_tac] sg hyps xs
+	       [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
+		Data.numeral_simp_tac ss] thy hyps xs
 	       (t', Data.mk_bal (Data.mk_sum T terms1', 
 				 newshape(n2-n1,terms2'))))
   end
diff -r d3f9abe00712 -r b2a894562b8f src/Provers/Arith/combine_numerals.ML
--- a/src/Provers/Arith/combine_numerals.ML	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Mon Aug 01 19:20:26 2005 +0200
@@ -27,17 +27,17 @@
   (*rules*)
   val left_distrib: thm
   (*proof tools*)
-  val prove_conv: tactic list -> Sign.sg -> string list -> term * term -> thm option
-  val trans_tac: thm option -> tactic (*applies the initial lemma*)
-  val norm_tac: tactic                (*proves the initial lemma*)
-  val numeral_simp_tac: tactic        (*proves the final theorem*)
-  val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
+  val prove_conv: tactic list -> theory -> string list -> term * term -> thm option
+  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
+  val norm_tac: simpset -> tactic                (*proves the initial lemma*)
+  val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
+  val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
 end;
 
 
 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
   sig
-  val proc: Sign.sg -> simpset -> term -> thm option
+  val proc: theory -> simpset -> term -> thm option
   end 
 =
 struct
@@ -64,7 +64,7 @@
 	| NONE => find_repeated (tab, t::past, terms);
 
 (*the simplification procedure*)
-fun proc sg _ t =
+fun proc thy ss t =
   let (*first freeze any Vars in the term to prevent flex-flex problems*)
       val (t', xs) = Term.adhoc_freeze_vars t
       val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
@@ -73,15 +73,15 @@
 		       i + #m + j + k == #m + i + (j + k) *)
 	    if m=0 orelse n=0 then   (*trivial, so do nothing*)
 		raise TERM("combine_numerals", []) 
-	    else Data.prove_conv [Data.norm_tac] sg xs
+	    else Data.prove_conv [Data.norm_tac ss] thy xs
 			(t', 
 			 Data.mk_sum T ([Data.mk_coeff(m,u),
 				         Data.mk_coeff(n,u)] @ terms))
   in
-      Option.map Data.simplify_meta_eq
+      Option.map (Data.simplify_meta_eq ss)
 	 (Data.prove_conv 
-	    [Data.trans_tac reshape, rtac Data.left_distrib 1,
-	     Data.numeral_simp_tac] sg xs
+	    [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
+	     Data.numeral_simp_tac ss] thy xs
 	    (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
   end
   handle TERM _ => NONE
diff -r d3f9abe00712 -r b2a894562b8f src/Provers/Arith/extract_common_term.ML
--- a/src/Provers/Arith/extract_common_term.ML	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/Provers/Arith/extract_common_term.ML	Mon Aug 01 19:20:26 2005 +0200
@@ -23,34 +23,34 @@
   val dest_bal: term -> term * term
   val find_first: term -> term list -> term list
   (*proof tools*)
-  val prove_conv: tactic list -> Sign.sg -> 
+  val prove_conv: tactic list -> theory -> 
                   thm list -> string list -> term * term -> thm option
-  val norm_tac: tactic                (*proves the result*)
-  val simplify_meta_eq: thm -> thm    (*simplifies the result*)
+  val norm_tac: simpset -> tactic                (*proves the result*)
+  val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the result*)
 end;
 
 
 functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA):
   sig
-  val proc: Sign.sg -> simpset -> term -> thm option
+  val proc: theory -> simpset -> term -> thm option
   end 
 =
 struct
 
 (*Store the term t in the table*)
-fun update_by_coeff (tab, t) = Termtab.update ((t, ()), tab);
+fun update_by_coeff t tab = Termtab.update ((t, ()), tab);
 
 (*a left-to-right scan of terms1, seeking a term u that is also in terms2*)
 fun find_common (terms1,terms2) =
-  let val tab2 = Library.foldl update_by_coeff (Termtab.empty, terms2)
+  let val tab2 = fold update_by_coeff terms2 Termtab.empty
       fun seek [] = raise TERM("find_common", []) 
 	| seek (u::terms) =
-	      if isSome (Termtab.lookup (tab2, u)) then u
+	      if Termtab.defined tab2 u then u
 	      else seek terms
-  in  seek terms1 end;
+  in seek terms1 end;
 
 (*the simplification procedure*)
-fun proc sg ss t =
+fun proc thy ss t =
   let
       val hyps = prems_of_ss ss;
       (*first freeze any Vars in the term to prevent flex-flex problems*)
@@ -63,12 +63,12 @@
       and terms2' = Data.find_first u terms2
       and T = Term.fastype_of u
       val reshape = 
-	    Data.prove_conv [Data.norm_tac] sg hyps xs
+	    Data.prove_conv [Data.norm_tac ss] thy hyps xs
 	        (t', 
 		 Data.mk_bal (Data.mk_sum T (u::terms1'), 
 		              Data.mk_sum T (u::terms2')))
   in
-      Option.map Data.simplify_meta_eq reshape
+      Option.map (Data.simplify_meta_eq ss) reshape
   end
   handle TERM _ => NONE
        | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
diff -r d3f9abe00712 -r b2a894562b8f src/ZF/Datatype.ML
--- a/src/ZF/Datatype.ML	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/ZF/Datatype.ML	Mon Aug 01 19:20:26 2005 +0200
@@ -62,9 +62,9 @@
         fold_bal FOLogic.mk_conj
                  (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
 
- val datatype_ss = simpset_of (the_context ());
+ val datatype_ss = simpset ();
 
- fun proc sg _ old =
+ fun proc sg ss old =
    let val _ = if !trace then writeln ("data_free: OLD = " ^ 
                                        string_of_cterm (cterm_of sg old))
                else ()
@@ -88,7 +88,7 @@
                else ();
        val goal = Logic.mk_equals (old, new)
        val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
-           simp_tac (datatype_ss addsimps #free_iffs lcon_info) 1)
+           simp_tac (Simplifier.inherit_bounds ss datatype_ss addsimps #free_iffs lcon_info) 1)
          handle ERROR_MESSAGE msg =>
          (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
           raise Match)
@@ -96,9 +96,8 @@
    handle Match => NONE;
 
 
- val conv = 
-     Simplifier.simproc (Theory.sign_of (theory "ZF")) "data_free" 
-                        ["(x::i) = y"] proc;
+ val conv = Simplifier.simproc (theory "ZF") "data_free" ["(x::i) = y"] proc;
+
 end;
 
 
diff -r d3f9abe00712 -r b2a894562b8f src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/ZF/Induct/Multiset.thy	Mon Aug 01 19:20:26 2005 +0200
@@ -483,14 +483,12 @@
 apply (rule int_of_diff, auto)
 done
 
-(*FIXME: we should not have to rename x to x' below!  There's a bug in the
-  interaction between simproc inteq_cancel_numerals and the simplifier.*)
 lemma setsum_decr2:
      "Finite(A)
       ==> \<forall>M. multiset(M) --> (\<forall>a \<in> mset_of(M).
-           setsum(%x'. $# mcount(funrestrict(M, mset_of(M)-{a}), x'), A) =
-           (if a \<in> A then setsum(%x'. $# mcount(M, x'), A) $- $# M`a
-            else setsum(%x'. $# mcount(M, x'), A)))"
+           setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}), x), A) =
+           (if a \<in> A then setsum(%x. $# mcount(M, x), A) $- $# M`a
+            else setsum(%x. $# mcount(M, x), A)))"
 apply (simp add: multiset_def)
 apply (erule Finite_induct)
 apply (auto simp add: multiset_fun_iff mcount_def mset_of_def)
diff -r d3f9abe00712 -r b2a894562b8f src/ZF/Integ/int_arith.ML
--- a/src/ZF/Integ/int_arith.ML	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/ZF/Integ/int_arith.ML	Mon Aug 01 19:20:26 2005 +0200
@@ -224,19 +224,21 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff 1
   val find_first_coeff  = find_first_coeff []
-  val trans_tac         = ArithData.gen_trans_tac iff_trans
+  fun trans_tac _       = ArithData.gen_trans_tac iff_trans
   val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
                                     zminus_simps@zadd_ac
   val norm_tac_ss2 = ZF_ss addsimps bin_simps@int_mult_minus_simps@intifys
   val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@
                                     zadd_ac@zmult_ac@tc_rules@intifys
-  val norm_tac          = ALLGOALS (asm_simp_tac norm_tac_ss1)
-                          THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
-                          THEN ALLGOALS (asm_simp_tac norm_tac_ss3)
-  val numeral_simp_tac  =
-         ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps@tc_rules@intifys))
-         THEN ALLGOALS Asm_simp_tac
-  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s@mult_1s)
+  fun norm_tac ss =
+    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
+    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
+    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss3))
+  fun numeral_simp_tac ss =
+    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss ZF_ss addsimps
+      add_0s @ bin_simps @ tc_rules @ intifys))
+    THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_bounds ss simpset)))
+  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   end;
 
 
@@ -298,17 +300,19 @@
   val dest_coeff        = dest_coeff 1
   val left_distrib      = left_zadd_zmult_distrib RS trans
   val prove_conv        = prove_conv_nohyps "int_combine_numerals"
-  val trans_tac         = ArithData.gen_trans_tac trans
+  fun trans_tac _       = ArithData.gen_trans_tac trans
   val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
                                     zminus_simps@zadd_ac@intifys
   val norm_tac_ss2 = ZF_ss addsimps bin_simps@int_mult_minus_simps@intifys
   val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@
                                     zadd_ac@zmult_ac@tc_rules@intifys
-  val norm_tac          = ALLGOALS (asm_simp_tac norm_tac_ss1)
-                          THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
-                          THEN ALLGOALS (asm_simp_tac norm_tac_ss3)
-  val numeral_simp_tac  =
-         ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps@tc_rules@intifys))
+  fun norm_tac ss =
+    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
+    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
+    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss3))
+  fun numeral_simp_tac ss =
+    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss ZF_ss addsimps
+      add_0s @ bin_simps @ tc_rules @ intifys))
   val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s@mult_1s)
   end;
 
@@ -335,14 +339,16 @@
   fun dest_coeff t = (dest_numeral t, one)  (*We ONLY want pure numerals.*)
   val left_distrib      = zmult_assoc RS sym RS trans
   val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
-  val trans_tac         = ArithData.gen_trans_tac trans
+  fun trans_tac _       = ArithData.gen_trans_tac trans
   val norm_tac_ss1 = ZF_ss addsimps mult_1s@diff_simps@zminus_simps
   val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
                                     bin_simps@zmult_ac@tc_rules@intifys
-  val norm_tac          = ALLGOALS (asm_simp_tac norm_tac_ss1)
-                          THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
-  val numeral_simp_tac  =
-         ALLGOALS (simp_tac (ZF_ss addsimps bin_simps@tc_rules@intifys))
+  fun norm_tac ss =
+    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
+    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
+  fun numeral_simp_tac ss =
+    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss ZF_ss addsimps
+      bin_simps @ tc_rules @ intifys))
   val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s)
   end;
 
diff -r d3f9abe00712 -r b2a894562b8f src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/ZF/arith_data.ML	Mon Aug 01 19:20:26 2005 +0200
@@ -14,7 +14,7 @@
   val gen_trans_tac: thm -> thm option -> tactic
   val prove_conv: string -> tactic list -> Sign.sg ->
                   thm list -> string list -> term * term -> thm option
-  val simplify_meta_eq: thm list -> thm -> thm
+  val simplify_meta_eq: thm list -> simpset -> thm -> thm
   (*debugging*)
   structure EqCancelNumeralsData   : CANCEL_NUMERALS_DATA
   structure LessCancelNumeralsData : CANCEL_NUMERALS_DATA
@@ -128,9 +128,9 @@
                diff_natify1, diff_natify2];
 
 (*Final simplification: cancel + and **)
-fun simplify_meta_eq rules =
+fun simplify_meta_eq rules ss =
     mk_meta_eq o
-    simplify (FOL_ss addeqcongs[eq_cong2,iff_cong2]
+    simplify (Simplifier.inherit_bounds ss FOL_ss addeqcongs[eq_cong2,iff_cong2]
                      delsimps iff_simps (*these could erase the whole rule!*)
                      addsimps rules);
 
@@ -143,13 +143,14 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val find_first_coeff  = find_first_coeff []
-  val norm_tac_ss1 = ZF_ss addsimps add_0s@add_succs@mult_1s@add_ac
-  val norm_tac_ss2 = ZF_ss addsimps add_0s@mult_1s@
-                                    add_ac@mult_ac@tc_rules@natifys
-  val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
-                 THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
-  val numeral_simp_tac_ss = ZF_ss addsimps add_0s@tc_rules@natifys
-  val numeral_simp_tac  = ALLGOALS (asm_simp_tac numeral_simp_tac_ss)
+  val norm_tac_ss1      = ZF_ss addsimps add_0s @ add_succs @ mult_1s @ add_ac
+  val norm_tac_ss2      = ZF_ss addsimps add_0s @ mult_1s @ add_ac @ mult_ac @ tc_rules @ natifys
+  fun norm_tac ss =
+    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
+    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
+  val numeral_simp_tac_ss = ZF_ss addsimps add_0s @ tc_rules @ natifys
+  fun numeral_simp_tac ss =
+    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss numeral_simp_tac_ss))
   val simplify_meta_eq  = simplify_meta_eq final_rules
   end;
 
@@ -164,7 +165,7 @@
   val dest_bal = FOLogic.dest_eq
   val bal_add1 = eq_add_iff RS iff_trans
   val bal_add2 = eq_add_iff RS iff_trans
-  val trans_tac = gen_trans_tac iff_trans
+  fun trans_tac _ = gen_trans_tac iff_trans
   end;
 
 structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData);
@@ -177,7 +178,7 @@
   val dest_bal = FOLogic.dest_bin "Ordinal.lt" iT
   val bal_add1 = less_add_iff RS iff_trans
   val bal_add2 = less_add_iff RS iff_trans
-  val trans_tac = gen_trans_tac iff_trans
+  fun trans_tac _ = gen_trans_tac iff_trans
   end;
 
 structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData);
@@ -190,7 +191,7 @@
   val dest_bal = FOLogic.dest_bin "Arith.diff" iT
   val bal_add1 = diff_add_eq RS trans
   val bal_add2 = diff_add_eq RS trans
-  val trans_tac = gen_trans_tac trans
+  fun trans_tac _ = gen_trans_tac trans
   end;
 
 structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData);