generalize CombineNumerals functor to allow coefficients with types other than IntInf.int

--- a/src/HOL/Integ/int_arith1.ML	Mon May 21 18:53:04 2007 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Mon May 21 19:05:37 2007 +0200
@@ -383,6 +383,8 @@
 
 structure CombineNumeralsData =
   struct
+  type coeff            = IntInf.int
+  val iszero            = (fn x => x = 0)
   val add               = IntInf.+ 
   val mk_sum            = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   val dest_sum          = dest_sum

--- a/src/HOL/Integ/nat_simprocs.ML	Mon May 21 18:53:04 2007 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Mon May 21 19:05:37 2007 +0200
@@ -234,6 +234,8 @@
 
 structure CombineNumeralsData =
   struct
+  type coeff            = IntInf.int
+  val iszero            = (fn x => x = 0)
   val add               = IntInf.+
   val mk_sum            = (fn T:typ => long_mk_sum)  (*to work for 2*x + 3*x *)
   val dest_sum          = dest_Sucs_sum false

--- a/src/Provers/Arith/combine_numerals.ML	Mon May 21 18:53:04 2007 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Mon May 21 19:05:37 2007 +0200
@@ -19,11 +19,13 @@
 signature COMBINE_NUMERALS_DATA =
 sig
   (*abstract syntax*)
-  val add: IntInf.int * IntInf.int -> IntInf.int     (*addition (or multiplication) *)
+  eqtype coeff
+  val iszero: coeff -> bool
+  val add: coeff * coeff -> coeff     (*addition (or multiplication) *)
   val mk_sum: typ -> term list -> term
   val dest_sum: term -> term list
-  val mk_coeff: IntInf.int * term -> term
-  val dest_coeff: term -> IntInf.int * term
+  val mk_coeff: coeff * term -> term
+  val dest_coeff: term -> coeff * term
   (*rules*)
   val left_distrib: thm
   (*proof tools*)
@@ -75,7 +77,7 @@
 
     val reshape =  (*Move i*u to the front and put j*u into standard form
                        i + #m + j + k == #m + i + (j + k) *)
-      if m=0 orelse n=0 then   (*trivial, so do nothing*)
+      if Data.iszero m orelse Data.iszero n then   (*trivial, so do nothing*)
         raise TERM("combine_numerals", [])
       else Data.prove_conv [Data.norm_tac ss] ctxt
         (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms))