1.1 --- a/src/ZF/Integ/int_arith.ML	Sat Feb 14 02:06:12 2004 +0100
     1.2 +++ b/src/ZF/Integ/int_arith.ML	Sun Feb 15 10:46:37 2004 +0100
     1.3 @@ -219,7 +219,7 @@
     1.4  
     1.5  structure CancelNumeralsCommon =
     1.6    struct
     1.7 -  val mk_sum            = mk_sum
     1.8 +  val mk_sum            = (fn T:typ => mk_sum)
     1.9    val dest_sum          = dest_sum
    1.10    val mk_coeff          = mk_coeff
    1.11    val dest_coeff        = dest_coeff 1
    1.12 @@ -292,7 +292,7 @@
    1.13  structure CombineNumeralsData =
    1.14    struct
    1.15    val add               = op + : int*int -> int
    1.16 -  val mk_sum            = long_mk_sum    (*to work for e.g. #2*x $+ #3*x *)
    1.17 +  val mk_sum            = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
    1.18    val dest_sum          = dest_sum
    1.19    val mk_coeff          = mk_coeff
    1.20    val dest_coeff        = dest_coeff 1
    1.21 @@ -328,7 +328,7 @@
    1.22  structure CombineNumeralsProdData =
    1.23    struct
    1.24    val add               = op * : int*int -> int
    1.25 -  val mk_sum            = mk_prod
    1.26 +  val mk_sum            = (fn T:typ => mk_prod)
    1.27    val dest_sum          = dest_prod
    1.28    fun mk_coeff(k,t) = if t=one then mk_numeral k
    1.29                        else raise TERM("mk_coeff", [])