src/ZF/Integ/int_arith.ML
changeset 15965 f422f8283491
parent 14387 e96d5c42c4b0
child 16973 b2a894562b8f
     1.1 --- a/src/ZF/Integ/int_arith.ML	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/src/ZF/Integ/int_arith.ML	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -291,7 +291,7 @@
     1.4  
     1.5  structure CombineNumeralsData =
     1.6    struct
     1.7 -  val add               = op + : int*int -> int
     1.8 +  val add               = IntInf.+ 
     1.9    val mk_sum            = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
    1.10    val dest_sum          = dest_sum
    1.11    val mk_coeff          = mk_coeff
    1.12 @@ -327,7 +327,7 @@
    1.13  
    1.14  structure CombineNumeralsProdData =
    1.15    struct
    1.16 -  val add               = op * : int*int -> int
    1.17 +  val add               = IntInf.*
    1.18    val mk_sum            = (fn T:typ => mk_prod)
    1.19    val dest_sum          = dest_prod
    1.20    fun mk_coeff(k,t) = if t=one then mk_numeral k