# HG changeset patch
# User huffman
# Date 1316106756 25200
# Node ID b36eedcd163302e1c9abc6b0b1b918ff9c916169
# Parent  e1139e612b5551c39b3d957d58352d8fff4fe1ec
numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting if-then-else

diff -r e1139e612b55 -r b36eedcd1633 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Thu Sep 15 17:06:00 2011 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Sep 15 10:12:36 2011 -0700
@@ -361,9 +361,9 @@
   val dest_coeff        = dest_coeff 1
   fun trans_tac _       = Arith_Data.trans_tac
 
-  val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
-  val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
-  val norm_ss3 = HOL_ss addsimps @{thms mult_ac}
+  val norm_ss1 = HOL_basic_ss addsimps minus_from_mult_simps @ mult_1s
+  val norm_ss2 = HOL_basic_ss addsimps simps @ mult_minus_simps
+  val norm_ss3 = HOL_basic_ss addsimps @{thms 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))