inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);

--- a/NEWS	Wed Oct 19 15:41:12 2011 +0200
+++ b/NEWS	Wed Oct 19 15:42:43 2011 +0200
@@ -28,6 +28,7 @@
   zadd_commute ~> add_commute
   zadd_assoc ~> add_assoc
   zadd_left_commute ~> add_left_commute
+  zadd_ac ~> add_ac
   zmult_ac ~> mult_ac
   zadd_0 ~> add_0_left
   zadd_0_right ~> add_0_right

--- a/src/HOL/Int.thy	Wed Oct 19 15:41:12 2011 +0200
+++ b/src/HOL/Int.thy	Wed Oct 19 15:42:43 2011 +0200
@@ -2390,9 +2390,6 @@
 
 subsection {* Legacy theorems *}
 
-(* used by Tools/Qelim/cooper.ML *)
-lemmas zadd_ac = add_ac [where 'a=int]
-
 lemmas inj_int = inj_of_nat [where 'a=int]
 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
 lemmas int_mult = of_nat_mult [where 'a=int]

--- a/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 19 15:41:12 2011 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 19 15:42:43 2011 +0200
@@ -74,7 +74,8 @@
 val false_tm = @{cterm "False"};
 val zdvd1_eq = @{thm "zdvd1_eq"};
 val presburger_ss = @{simpset} addsimps [zdvd1_eq];
-val lin_ss = presburger_ss addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms zadd_ac});
+val lin_ss =
+  presburger_ss addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms add_ac [where 'a=int]});
 
 val iT = HOLogic.intT
 val bT = HOLogic.boolT;