src/HOL/Tools/numeral_simprocs.ML

     [@{thm mult.assoc}, @{thm minus_mult_right}, @{thm minus_mult_commute}];
 
 val norm_ss1 =
   simpset_of (put_simpset num_ss @{context}
     addsimps numeral_syms @ add_0s @ mult_1s @
-    diff_simps @ minus_simps @ @{thms add_ac})
+    diff_simps @ minus_simps @ @{thms ac_simps})
 
 val norm_ss2 =
   simpset_of (put_simpset num_ss @{context}
     addsimps non_add_simps @ mult_minus_simps)
 
 val norm_ss3 =
   simpset_of (put_simpset num_ss @{context}
-    addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac minus_mult_commute})
+    addsimps minus_from_mult_simps @ @{thms ac_simps} @ @{thms ac_simps minus_mult_commute})
 
 structure CancelNumeralsCommon =
 struct
   val mk_sum = mk_sum
   val dest_sum = dest_sum

 
 (*We do not need folding for addition: combine_numerals does the same thing*)
 
 structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
 struct
-  val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac minus_mult_commute})
+  val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms ac_simps minus_mult_commute})
   val eq_reflection = eq_reflection
   val is_numeral = can HOLogic.dest_number
 end;
 
 structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);

   val norm_ss1 =
     simpset_of (put_simpset HOL_basic_ss @{context} addsimps minus_from_mult_simps @ mult_1s)
   val norm_ss2 =
     simpset_of (put_simpset HOL_basic_ss @{context} addsimps simps @ mult_minus_simps)
   val norm_ss3 =
-    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac minus_mult_commute})
+    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms ac_simps minus_mult_commute})
   fun norm_tac ctxt =
     ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
     THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt))
 

   val mk_coeff = mk_coeff
   val dest_coeff = dest_coeff
   val find_first = find_first_t []
   val trans_tac = trans_tac
   val norm_ss =
-    simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms mult_ac minus_mult_commute})
+    simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms ac_simps minus_mult_commute})
   fun norm_tac ctxt =
     ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
   val simplify_meta_eq  = cancel_simplify_meta_eq 
   fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
 end;