src/HOL/Tools/Presburger/cooper_dec.ML

 signature COOPER_DEC = 
 sig
   exception COOPER
   exception COOPER_ORACLE of term
   val is_arith_rel : term -> bool
-  val mk_numeral : int -> term
-  val dest_numeral : term -> int
+  val mk_numeral : IntInf.int -> term
+  val dest_numeral : term -> IntInf.int
   val is_numeral : term -> bool
   val zero : term
   val one : term
-  val linear_cmul : int -> term -> term
+  val linear_cmul : IntInf.int -> term -> term
   val linear_add : string list -> term -> term -> term 
   val linear_sub : string list -> term -> term -> term 
   val linear_neg : term -> term
   val lint : string list -> term -> term
   val linform : string list -> term -> term
-  val formlcm : term -> term -> int
-  val adjustcoeff : term -> int -> term -> term
+  val formlcm : term -> term -> IntInf.int
+  val adjustcoeff : term -> IntInf.int -> term -> term
   val unitycoeff : term -> term -> term
-  val divlcm : term -> term -> int
+  val divlcm : term -> term -> IntInf.int
   val bset : term -> term -> term list
   val aset : term -> term -> term list
   val linrep : string list -> term -> term -> term -> term
   val list_disj : term list -> term
   val list_conj : term list -> term
   val simpl : term -> term
   val fv : term -> string list
   val negate : term -> term
-  val operations : (string * (int * int -> bool)) list
+  val operations : (string * (IntInf.int * IntInf.int -> bool)) list
   val conjuncts : term -> term list
   val disjuncts : term -> term list
   val has_bound : term -> bool
   val minusinf : term -> term -> term
   val plusinf : term -> term -> term

 (* ------------------------------------------------------------------------- *) 
 (* Lift operations up to numerals.                                           *) 
 (* ------------------------------------------------------------------------- *) 
  
 (*Assumption : The construction of atomar formulas in linearl arithmetic is based on 
-relation operations of Type : [int,int]---> bool *) 
+relation operations of Type : [IntInf.int,IntInf.int]---> bool *) 
  
 (* ------------------------------------------------------------------------- *) 
  
 (*Function is_arith_rel returns true if and only if the term is an atomar presburger 
 formula *) 

  
 (*Transform a natural number to a term*) 
  
 fun mk_numeral 0 = Const("0",HOLogic.intT)
    |mk_numeral 1 = Const("1",HOLogic.intT)
-   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin (IntInf.fromInt n)); 
+   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin n); 
  
 (*Transform an Term to an natural number*)	  
 	  
 fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
    |dest_numeral (Const ("Numeral.number_of",_) $ n) = 
-       IntInf.toInt (HOLogic.dest_binum n);
+       HOLogic.dest_binum n;
 (*Some terms often used for pattern matching*) 
  
 val zero = mk_numeral 0; 
 val one = mk_numeral 1; 
  

 (* Operations on canonical linear terms c1 * x1 + ... + cn * xn + k          *) 
 (*                                                                           *) 
 (* Note that we're quite strict: the ci must be present even if 1            *) 
 (* (but if 0 we expect the monomial to be omitted) and k must be there       *) 
 (* even if it's zero. Thus, it's a constant iff not an addition term.        *) 
-(* ------------------------------------------------------------------------- *) 
+(* ------------------------------------------------------------------------- *)  
  
  
 fun linear_cmul n tm =  if n = 0 then zero else let fun times n k = n*k in  
   ( case tm of  
      (Const("op +",T)  $  (Const ("op *",T1 ) $c1 $  x1) $ rest) =>