src/HOL/Integ/nat_simprocs.ML
changeset 15965 f422f8283491
parent 15921 b6e345548913
child 16973 b2a894562b8f
     1.1 --- a/src/HOL/Integ/nat_simprocs.ML	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  fun dest_numeral (Const ("0", _)) = 0
     1.5    | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
     1.6    | dest_numeral (Const("Numeral.number_of", _) $ w) =
     1.7 -      (BasisLibrary.Int.max (0, HOLogic.dest_binum w)
     1.8 +      (IntInf.max (0, HOLogic.dest_binum w)
     1.9         handle TERM _ => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
    1.10    | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
    1.11  
    1.12 @@ -245,7 +245,7 @@
    1.13  
    1.14  structure CombineNumeralsData =
    1.15    struct
    1.16 -  val add               = op + : int*int -> int
    1.17 +  val add               = IntInf.+
    1.18    val mk_sum            = (fn T:typ => long_mk_sum)  (*to work for 2*x + 3*x *)
    1.19    val dest_sum          = restricted_dest_Sucs_sum
    1.20    val mk_coeff          = mk_coeff