# HG changeset patch
# User chaieb
# Date 1181552773 -7200
# Node ID 90be000da2a71dc89a2da112f0d7cca83e5d51aa
# Parent  26c978a475de554cac83fd4617457104ad6b459c
Temporarily use int instead of IntInf.int but Code generator should map HOL's int to ML's IntInf.int --- To be fixed

diff -r 26c978a475de -r 90be000da2a7 src/HOL/Complex/ex/linreif.ML
--- a/src/HOL/Complex/ex/linreif.ML	Mon Jun 11 11:06:11 2007 +0200
+++ b/src/HOL/Complex/ex/linreif.ML	Mon Jun 11 11:06:13 2007 +0200
@@ -26,7 +26,7 @@
       | Const("RealDef.real",_)$ @{term "1::int"} => C 1
       | @{term "0::real"} => C 0
       | @{term "0::real"} => C 1
-      | Term.Bound i => Bound (nat (IntInf.fromInt i))
+      | Term.Bound i => Bound (nat i)
       | Const(@{const_name "HOL.uminus"},_)$t' => Neg (num_of_term vs t')
       | Const (@{const_name "HOL.plus"},_)$t1$t2 => Add (num_of_term vs t1,num_of_term vs t2)
       | Const (@{const_name "HOL.minus"},_)$t1$t2 => Sub (num_of_term vs t1,num_of_term vs t2)
@@ -55,9 +55,9 @@
       | Const("op -->",_)$t1$t2 => Imp(fm_of_term vs t1,fm_of_term vs t2)
       | Const("Not",_)$t' => NOT(fm_of_term vs t')
       | Const("Ex",_)$Term.Abs(xn,xT,p) => 
-	E(fm_of_term (map (fn(v,n) => (v,Suc n)) vs) p)
+	E(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
       | Const("All",_)$Term.Abs(xn,xT,p) => 
-	A(fm_of_term (map (fn(v,n) => (v,Suc n)) vs) p)
+	A(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
       | _ => error ("fm_of_term : unknown term!" ^ (Display.raw_string_of_term t));
 
 fun zip [] [] = []
@@ -66,7 +66,7 @@
 
 fun start_vs t =
     let val fs = term_frees t
-    in zip fs (map (nat o IntInf.fromInt) (0 upto  (length fs - 1)))
+    in zip fs (map nat (0 upto  (length fs - 1)))
     end ;
 
 (* transform num and fm back to terms *)
diff -r 26c978a475de -r 90be000da2a7 src/HOL/Complex/ex/mireif.ML
--- a/src/HOL/Complex/ex/mireif.ML	Mon Jun 11 11:06:11 2007 +0200
+++ b/src/HOL/Complex/ex/mireif.ML	Mon Jun 11 11:06:13 2007 +0200
@@ -28,7 +28,7 @@
       | Const("RealDef.real",_)$ @{term "1::int"} => C 1
       | @{term "0::real"} => C 0
       | @{term "1::real"} => C 1
-      | Term.Bound i => Bound (nat (IntInf.fromInt i))
+      | Term.Bound i => Bound (nat i)
       | Const(@{const_name "HOL.uminus"},_)$t' => Neg (num_of_term vs t')
       | Const (@{const_name "HOL.plus"},_)$t1$t2 => Add (num_of_term vs t1,num_of_term vs t2)
       | Const (@{const_name "HOL.minus"},_)$t1$t2 => Sub (num_of_term vs t1,num_of_term vs t2)
@@ -72,7 +72,7 @@
 
 fun start_vs t =
     let val fs = term_frees t
-    in zip fs (map (nat o IntInf.fromInt) (0 upto  (length fs - 1)))
+    in zip fs (map nat (0 upto  (length fs - 1)))
     end ;
 
 (* transform num and fm back to terms *)
diff -r 26c978a475de -r 90be000da2a7 src/HOL/ex/coopereif.ML
--- a/src/HOL/ex/coopereif.ML	Mon Jun 11 11:06:11 2007 +0200
+++ b/src/HOL/ex/coopereif.ML	Mon Jun 11 11:06:13 2007 +0200
@@ -17,7 +17,7 @@
 			 | SOME n => Bound n)
       | @{term "0::int"} => C 0
       | @{term "1::int"} => C 1
-      | Term.Bound i => Bound (nat (IntInf.fromInt i))
+      | Term.Bound i => Bound (nat i)
       | Const(@{const_name "HOL.uminus"},_)$t' => Neg (i_of_term vs t')
       | Const(@{const_name "HOL.plus"},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
       | Const(@{const_name "HOL.minus"},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
@@ -79,8 +79,8 @@
 let
  val fs = term_frees t
  val ps = term_bools [] t
-in (fs ~~ (map (nat o IntInf.fromInt) (0 upto  (length fs - 1))),
-    ps ~~ (map (nat o IntInf.fromInt) (0 upto  (length ps - 1))))
+in (fs ~~ (map nat (0 upto  (length fs - 1))),
+    ps ~~ (map nat (0 upto  (length ps - 1))))
 end ;
 
 val iT = HOLogic.intT;