The SMLNJ Problem fixed...

--- a/src/HOL/Integ/reflected_cooper.ML	Thu Sep 15 20:38:47 2005 +0200
+++ b/src/HOL/Integ/reflected_cooper.ML	Thu Sep 15 22:16:23 2005 +0200
@@ -15,7 +15,7 @@
 			 | SOME n => Var n)
       | Const("0",iT) => Cst 0
       | Const("1",iT) => Cst 1
-      | Bound i => Var (nat i)
+      | Bound i => Var (nat (IntInf.fromInt i))
       | Const("uminus",_)$t' => Neg (i_of_term vs t')
       | Const ("op +",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
       | Const ("op -",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
@@ -61,7 +61,7 @@
 
 fun start_vs t =
     let val fs = term_frees t
-    in zip fs (map nat (0 upto (length fs - 1)))
+    in zip fs (map (nat o IntInf.fromInt) (0 upto  (length fs - 1)))
     end ;
 
 (* transform intterm and QF back to terms *)
@@ -121,4 +121,4 @@
       | Some t' => HOLogic.mk_Trueprop (HOLogic.mk_eq(t,t'))
     end ;
  
-end;
\ No newline at end of file
+end;

--- a/src/HOL/Tools/Presburger/reflected_cooper.ML	Thu Sep 15 20:38:47 2005 +0200
+++ b/src/HOL/Tools/Presburger/reflected_cooper.ML	Thu Sep 15 22:16:23 2005 +0200
@@ -15,7 +15,7 @@
 			 | SOME n => Var n)
       | Const("0",iT) => Cst 0
       | Const("1",iT) => Cst 1
-      | Bound i => Var (nat i)
+      | Bound i => Var (nat (IntInf.fromInt i))
       | Const("uminus",_)$t' => Neg (i_of_term vs t')
       | Const ("op +",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
       | Const ("op -",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
@@ -61,7 +61,7 @@
 
 fun start_vs t =
     let val fs = term_frees t
-    in zip fs (map nat (0 upto (length fs - 1)))
+    in zip fs (map (nat o IntInf.fromInt) (0 upto  (length fs - 1)))
     end ;
 
 (* transform intterm and QF back to terms *)
@@ -121,4 +121,4 @@
       | Some t' => HOLogic.mk_Trueprop (HOLogic.mk_eq(t,t'))
     end ;
  
-end;
\ No newline at end of file
+end;