--- a/src/HOL/Complex/ex/linreif.ML Mon Jul 16 09:29:00 2007 +0200
+++ b/src/HOL/Complex/ex/linreif.ML Mon Jul 16 09:29:01 2007 +0200
@@ -9,7 +9,8 @@
struct
open Ferrack;
-open ReflectedFerrack
+
+val nat = Ferrack.nat o Integer.int;
exception LINR;
@@ -29,7 +30,7 @@
| 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)
@@ -69,7 +70,7 @@
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 *)