simprocs: static evaluation of simpset;

--- a/src/HOL/Integ/int_arith1.ML	Thu Dec 01 22:03:06 2005 +0100
+++ b/src/HOL/Integ/int_arith1.ML	Thu Dec 01 22:04:27 2005 +0100
@@ -308,9 +308,9 @@
 fun trans_tac NONE      = all_tac
   | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
 
-fun simplify_meta_eq rules ss =
-    simplify (Simplifier.inherit_context ss HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
-    o mk_meta_eq;
+fun simplify_meta_eq rules =
+  let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules
+  in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
 
 structure CancelNumeralsCommon =
   struct
@@ -320,15 +320,18 @@
   val dest_coeff        = dest_coeff 1
   val find_first_coeff  = find_first_coeff []
   val trans_tac         = fn _ => trans_tac
+
+  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
+    diff_simps @ minus_simps @ add_ac
+  val norm_ss2 = num_ss addsimps non_add_bin_simps @ mult_minus_simps
+  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
   fun norm_tac ss =
-    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_context ss HOL_ss addsimps add_0s @ bin_simps))
+    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
+    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
+    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
+
+  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps
+  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
   end;
 
@@ -398,15 +401,18 @@
   val left_distrib      = combine_common_factor RS trans
   val prove_conv        = Bin_Simprocs.prove_conv_nohyps
   val trans_tac         = fn _ => trans_tac
+
+  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
+    diff_simps @ minus_simps @ add_ac
+  val norm_ss2 = num_ss addsimps non_add_bin_simps @ mult_minus_simps
+  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
   fun norm_tac ss =
-    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_context ss HOL_ss addsimps add_0s @ bin_simps))
+    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
+    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
+    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
+
+  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps
+  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
   end;
 

--- a/src/HOL/Integ/int_factor_simprocs.ML	Thu Dec 01 22:03:06 2005 +0100
+++ b/src/HOL/Integ/int_factor_simprocs.ML	Thu Dec 01 22:04:27 2005 +0100
@@ -43,14 +43,17 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff 1
   val trans_tac         = fn _ => trans_tac
+
+  val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
+  val norm_ss2 = HOL_ss addsimps bin_simps@mult_minus_simps
+  val norm_ss3 = HOL_ss addsimps mult_ac
   fun norm_tac ss =
-    let val HOL_ss' = Simplifier.inherit_context 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_context ss HOL_ss addsimps rel_number_of @ bin_simps))
+    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
+    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
+    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
+
+  val numeral_simp_ss = HOL_ss addsimps rel_number_of @ bin_simps
+  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq = 
 	Int_Numeral_Simprocs.simplify_meta_eq
 	     [add_0, add_0_right,
@@ -250,8 +253,8 @@
   val dest_coeff        = dest_coeff
   val find_first        = find_first []
   val trans_tac         = fn _ => trans_tac
-  fun norm_tac ss =
-    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps mult_1s @ mult_ac))
+  val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
+  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   end;
 
 (*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in

--- a/src/HOL/Integ/nat_simprocs.ML	Thu Dec 01 22:03:06 2005 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML	Thu Dec 01 22:04:27 2005 +0100
@@ -169,14 +169,16 @@
   val dest_coeff        = dest_coeff
   val find_first_coeff  = find_first_coeff []
   val trans_tac         = fn _ => trans_tac
-  fun norm_tac ss =
-    let val num_ss' = Simplifier.inherit_context 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))
-    end
-  fun numeral_simp_tac ss =
-    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
+
+  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
+    [Suc_eq_add_numeral_1_left] @ add_ac
+  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
+  fun norm_tac ss = 
+    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
+    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
+
+  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
+  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss));
   val simplify_meta_eq  = simplify_meta_eq
   end;
 
@@ -254,14 +256,15 @@
   val left_distrib      = left_add_mult_distrib RS trans
   val prove_conv        = Bin_Simprocs.prove_conv_nohyps
   val trans_tac         = fn _ => trans_tac
+
+  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [Suc_eq_add_numeral_1] @ add_ac
+  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
   fun norm_tac ss =
-    let val num_ss' = Simplifier.inherit_context 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))
-    end
-  fun numeral_simp_tac ss =
-    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
+    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
+    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
+
+  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
+  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq  = simplify_meta_eq
   end;
 
@@ -278,14 +281,16 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val trans_tac         = fn _ => trans_tac
+
+  val norm_ss1 = num_ss addsimps
+    numeral_syms @ add_0s @ mult_1s @ [Suc_eq_add_numeral_1_left] @ add_ac
+  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
   fun norm_tac ss =
-    let val num_ss' = Simplifier.inherit_context 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))
-    end
-  fun numeral_simp_tac ss =
-    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps bin_simps))
+    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
+    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
+
+  val numeral_simp_ss = HOL_ss addsimps bin_simps
+  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq  = simplify_meta_eq
   end
 
@@ -371,8 +376,8 @@
   val dest_coeff        = dest_coeff
   val find_first        = find_first []
   val trans_tac         = fn _ => trans_tac
-  fun norm_tac ss =
-    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps mult_1s @ mult_ac))
+  val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
+  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   end;
 
 structure EqCancelFactor = ExtractCommonTermFun

--- a/src/HOL/Product_Type.thy	Thu Dec 01 22:03:06 2005 +0100
+++ b/src/HOL/Product_Type.thy	Thu Dec 01 22:04:27 2005 +0100
@@ -401,7 +401,7 @@
 ML_setup {*
 
 local
-  val cond_split_eta = thm "cond_split_eta";
+  val cond_split_eta_ss = HOL_basic_ss addsimps [thm "cond_split_eta"]
   fun  Pair_pat k 0 (Bound m) = (m = k)
   |    Pair_pat k i (Const ("Pair",  _) $ Bound m $ t) = i > 0 andalso
                         m = k+i andalso Pair_pat k (i-1) t
@@ -415,7 +415,7 @@
   |   split_pat tp i _ = NONE;
   fun metaeq thy ss lhs rhs = mk_meta_eq (Goal.prove thy [] []
         (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
-        (K (simp_tac (Simplifier.inherit_context ss HOL_basic_ss addsimps [cond_split_eta]) 1)));
+        (K (simp_tac (Simplifier.inherit_context ss cond_split_eta_ss) 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

--- a/src/HOL/Set.thy	Thu Dec 01 22:03:06 2005 +0100
+++ b/src/HOL/Set.thy	Thu Dec 01 22:04:27 2005 +0100
@@ -426,24 +426,17 @@
 
 ML_setup {*
   local
-    val Ball_def = thm "Ball_def";
-    val Bex_def = thm "Bex_def";
-
-    val simpset = Simplifier.clear_ss HOL_basic_ss;
-    fun unfold_tac ss 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;
+    val unfold_bex_tac = unfold_tac [thm "Bex_def"];
+    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
     val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
 
-    fun prove_ball_tac ss =
-      unfold_tac ss Ball_def THEN Quantifier1.prove_one_point_all_tac;
+    val unfold_ball_tac = unfold_tac [thm "Ball_def"];
+    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
     val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
   in
-    val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+    val defBEX_regroup = Simplifier.simproc (the_context ())
       "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
-    val defBALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+    val defBALL_regroup = Simplifier.simproc (the_context ())
       "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
   end;
 

--- a/src/HOL/arith_data.ML	Thu Dec 01 22:03:06 2005 +0100
+++ b/src/HOL/arith_data.ML	Thu Dec 01 22:04:27 2005 +0100
@@ -59,8 +59,9 @@
 
 (* rewriting *)
 
-fun simp_all_tac rules ss =
-  ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps rules));
+fun simp_all_tac rules =
+  let val ss0 = HOL_ss addsimps rules
+  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
 
 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];
@@ -89,7 +90,9 @@
   val mk_sum = mk_norm_sum;
   val dest_sum = dest_sum;
   val prove_conv = prove_conv;
-  fun norm_tac ss = simp_all_tac add_rules ss THEN simp_all_tac add_ac ss;
+  val norm_tac1 = simp_all_tac add_rules;
+  val norm_tac2 = simp_all_tac add_ac;
+  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
 end;
 
 fun gen_uncancel_tac rule ct =

--- a/src/ZF/Integ/int_arith.ML	Thu Dec 01 22:03:06 2005 +0100
+++ b/src/ZF/Integ/int_arith.ML	Thu Dec 01 22:04:27 2005 +0100
@@ -225,18 +225,18 @@
   val dest_coeff        = dest_coeff 1
   val find_first_coeff  = find_first_coeff []
   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_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ zadd_ac
+  val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
+  val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ zadd_ac @ zmult_ac @ tc_rules @ intifys
   fun norm_tac ss =
-    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
-    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
-    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss3))
+    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
+    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
+    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
+
+  val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
   fun numeral_simp_tac ss =
-    ALLGOALS (simp_tac (Simplifier.inherit_context ss ZF_ss addsimps
-      add_0s @ bin_simps @ tc_rules @ intifys))
+    ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
     THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset)))
   val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   end;
@@ -301,19 +301,19 @@
   val left_distrib      = left_zadd_zmult_distrib RS trans
   val prove_conv        = prove_conv_nohyps "int_combine_numerals"
   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_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ zadd_ac @ intifys
+  val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
+  val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ zadd_ac @ zmult_ac @ tc_rules @ intifys
   fun norm_tac ss =
-    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
-    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
-    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss3))
+    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
+    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
+    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
+
+  val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
   fun numeral_simp_tac ss =
-    ALLGOALS (simp_tac (Simplifier.inherit_context ss ZF_ss addsimps
-      add_0s @ bin_simps @ tc_rules @ intifys))
-  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s@mult_1s)
+    ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
+  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   end;
 
 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
@@ -340,16 +340,18 @@
   val left_distrib      = zmult_assoc RS sym RS trans
   val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
   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_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps
+  val norm_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym] @
+    bin_simps @ zmult_ac @ tc_rules @ intifys
   fun norm_tac ss =
-    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
-    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
+    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
+    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
+
+  val numeral_simp_ss = ZF_ss addsimps bin_simps @ tc_rules @ intifys
   fun numeral_simp_tac ss =
-    ALLGOALS (simp_tac (Simplifier.inherit_context ss ZF_ss addsimps
-      bin_simps @ tc_rules @ intifys))
-  val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s)
+    ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
+  val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s);
   end;
 
 

--- a/src/ZF/arith_data.ML	Thu Dec 01 22:03:06 2005 +0100
+++ b/src/ZF/arith_data.ML	Thu Dec 01 22:04:27 2005 +0100
@@ -128,11 +128,12 @@
                diff_natify1, diff_natify2];
 
 (*Final simplification: cancel + and **)
-fun simplify_meta_eq rules ss =
-    mk_meta_eq o
-    simplify (Simplifier.inherit_context ss FOL_ss addeqcongs[eq_cong2,iff_cong2]
-                     delsimps iff_simps (*these could erase the whole rule!*)
-                     addsimps rules);
+fun simplify_meta_eq rules =
+  let val ss0 =
+    FOL_ss addeqcongs [eq_cong2, iff_cong2]
+      delsimps iff_simps (*these could erase the whole rule!*)
+      addsimps rules
+  in fn ss => mk_meta_eq o simplify (Simplifier.inherit_context ss ss0) end;
 
 val final_rules = add_0s @ mult_1s @ [mult_0, mult_0_right];
 
@@ -143,14 +144,15 @@
   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_ss1 = ZF_ss addsimps add_0s @ add_succs @ mult_1s @ add_ac
+  val norm_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_context ss norm_tac_ss1))
-    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
-  val numeral_simp_tac_ss = ZF_ss addsimps add_0s @ tc_rules @ natifys
+    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
+    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
+  val numeral_simp_ss = ZF_ss addsimps add_0s @ tc_rules @ natifys
   fun numeral_simp_tac ss =
-    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss numeral_simp_tac_ss))
+    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq  = simplify_meta_eq final_rules
   end;