# HG changeset patch
# User huffman
# Date 1316387563 25200
# Node ID 6e6e958b2d4034283c0021eace7c050b7150b4ec
# Parent  e7ac11643befb756fd660a084d229a7900a0fc93# Parent  b36eedcd163302e1c9abc6b0b1b918ff9c916169
merged

diff -r e7ac11643bef -r 6e6e958b2d40 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Sun Sep 18 21:41:36 2011 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Sun Sep 18 16:12:43 2011 -0700
@@ -367,9 +367,9 @@
   val dest_coeff = dest_coeff 1
   val trans_tac = 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))