diff -r 44c5419cd9f1 -r 815f3ccc0b45 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Fri Feb 15 23:22:02 2008 +0100
+++ b/src/HOL/Presburger.thy	Sat Feb 16 02:01:13 2008 +0100
@@ -671,20 +671,19 @@
   unfolding number_of_is_id ..
 
 lemmas pred_succ_numeral_code [code func] =
-  arith_simps(5-12)
+  pred_bin_simps succ_bin_simps
 
 lemmas plus_numeral_code [code func] =
-  arith_simps(13-17)
-  arith_simps(26-27)
+  add_bin_simps
   arith_extra_simps(1) [where 'a = int]
 
 lemmas minus_numeral_code [code func] =
-  arith_simps(18-21)
+  minus_bin_simps
   arith_extra_simps(2) [where 'a = int]
   arith_extra_simps(5) [where 'a = int]
 
 lemmas times_numeral_code [code func] =
-  arith_simps(22-25)
+  mult_bin_simps
   arith_extra_simps(4) [where 'a = int]
 
 lemmas eq_numeral_code [code func] =