--- a/src/HOL/arith_data.ML Wed Aug 02 01:48:09 2006 +0200
+++ b/src/HOL/arith_data.ML Wed Aug 02 03:33:28 2006 +0200
@@ -414,7 +414,7 @@
| domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
| domain_is_nat _ = false;
-fun number_of (n : int, T : typ) =
+fun number_of (n : IntInf.int, T : typ) =
HOLogic.number_of_const T $ (HOLogic.mk_binum n);
(*---------------------------------------------------------------------------*)
--- a/src/Provers/Arith/fast_lin_arith.ML Wed Aug 02 01:48:09 2006 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Aug 02 03:33:28 2006 +0200
@@ -498,7 +498,7 @@
fun coeff poly atom : IntInf.int =
AList.lookup (op =) poly atom |> the_default 0;
-fun lcms (is : int list) : int = Library.foldl lcm (1, is);
+fun lcms (is : IntInf.int list) : IntInf.int = Library.foldl lcm (1, is);
fun integ(rlhs,r,rel,rrhs,s,d) =
let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s