src/HOL/Integ/nat_simprocs.ML

--- 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