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