Efficient_Nat streamlined and improved

--- a/src/HOL/Complex/ex/linreif.ML	Mon Jan 21 08:43:37 2008 +0100
+++ b/src/HOL/Complex/ex/linreif.ML	Mon Jan 21 08:45:36 2008 +0100
@@ -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 i)
+      | Term.Bound i => Bound 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)
@@ -60,9 +60,9 @@
 
 
 fun start_vs t =
-    let val fs = term_frees t
-    in fs ~~ map nat (0 upto  (length fs - 1))
-    end ;
+  let
+    val fs = term_frees t
+  in fs ~~ (0 upto (length fs - 1)) end;
 
 (* transform num and fm back to terms *)
 
@@ -111,9 +111,8 @@
 (* The oracle *)
 
 fun linrqe_oracle thy t = 
-    let 
-	val vs = start_vs t
-    in HOLogic.mk_Trueprop (HOLogic.mk_eq(t, term_of_fm vs (linrqe (fm_of_term vs t))))
-    end;
+  let 
+    val vs = start_vs t
+  in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (linrqe (fm_of_term vs t)))) end;
 
 end;

--- a/src/HOL/ex/coopereif.ML	Mon Jan 21 08:43:37 2008 +0100
+++ b/src/HOL/ex/coopereif.ML	Mon Jan 21 08:45:36 2008 +0100
@@ -16,7 +16,7 @@
     | SOME n => Bound n)
     | @{term "0::int"} => C 0
     | @{term "1::int"} => C 1
-    | Term.Bound i => Bound (nat i)
+    | Term.Bound i => Bound 0
     | 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)
@@ -42,12 +42,12 @@
       | Const("Not",_)$t' => Not(qf_of_term ps vs t')
       | Const("Ex",_)$Abs(xn,xT,p) => 
          let val (xn',p') = variant_abs (xn,xT,p)
-             val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)
+             val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1 + n)) vs)
          in E (qf_of_term ps vs' p')
          end
       | Const("All",_)$Abs(xn,xT,p) => 
          let val (xn',p') = variant_abs (xn,xT,p)
-             val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)
+             val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1 + n)) vs)
          in A (qf_of_term ps vs' p')
          end
       | _ =>(case AList.lookup (op aconv) ps t of 
@@ -77,8 +77,7 @@
     val fs = term_frees t
     val ps = term_bools [] t
   in
-    (fs ~~ (map nat (0 upto  (length fs - 1))),
-      ps ~~ (map nat (0 upto  (length ps - 1))))
+    (fs ~~ (0 upto (length fs - 1)), ps ~~ (0 upto (length ps - 1)))
   end;
 
 fun term_of_i vs t = case t