src/HOL/Integ/int_arith1.ML
changeset 15965 f422f8283491
parent 15921 b6e345548913
child 16423 24abe4c0e4b4
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -149,8 +149,8 @@
     1.4  (*Order integers by absolute value and then by sign. The standard integer
     1.5    ordering is not well-founded.*)
     1.6  fun num_ord (i,j) =
     1.7 -      (case Int.compare (abs i, abs j) of
     1.8 -            EQUAL => Int.compare (Int.sign i, Int.sign j) 
     1.9 +      (case IntInf.compare (IntInf.abs i, IntInf.abs j) of
    1.10 +            EQUAL => Int.compare (IntInf.sign i, IntInf.sign j) 
    1.11            | ord => ord);
    1.12  
    1.13  (*This resembles Term.term_ord, but it puts binary numerals before other
    1.14 @@ -388,7 +388,7 @@
    1.15  
    1.16  structure CombineNumeralsData =
    1.17    struct
    1.18 -  val add               = op + : int*int -> int
    1.19 +  val add               = IntInf.+ 
    1.20    val mk_sum            = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
    1.21    val dest_sum          = dest_sum
    1.22    val mk_coeff          = mk_coeff