src/HOL/Complex/ex/linreif.ML

 
 structure ReflectedFerrack =
 struct
 
 open Ferrack;
-open ReflectedFerrack
+
+val nat = Ferrack.nat o Integer.int;
 
 exception LINR;
 
 (* pseudo reification : term -> intterm *)
 val iT = HOLogic.intT;

 			 | SOME n => Bound n)
       | Const("RealDef.real",_)$ @{term "0::int"} => C 0
       | Const("RealDef.real",_)$ @{term "1::int"} => C 1
       | @{term "0::real"} => C 0
       | @{term "0::real"} => C 1
-      | Term.Bound i => Bound (Integer.nat 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)
       | Const (@{const_name "HOL.times"},_)$t1$t2 => 
 	(case (num_of_term vs t1) of C i => 

   | zip (x::xs) (y::ys) = (x,y)::(zip xs ys);
 
 
 fun start_vs t =
     let val fs = term_frees t
-    in zip fs (map Integer.nat (0 upto  (length fs - 1)))
+    in zip fs (map nat (0 upto  (length fs - 1)))
     end ;
 
 (* transform num and fm back to terms *)
 
 fun myassoc2 l v =