diff -r ac9e909fe55d -r 0a2371e7ced3 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 15 08:31:30 2013 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 15 08:31:31 2013 +0100
@@ -6,7 +6,7 @@
 
 theory Parametric_Ferrante_Rackoff
 imports Reflected_Multivariate_Polynomial Dense_Linear_Order DP_Library
-  "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
+  "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
 begin
 
 subsection {* Terms *}
@@ -2795,6 +2795,10 @@
 fun binopT T = T --> T --> T;
 fun relT T = T --> T --> @{typ bool};
 
+val mk_C = @{code C} o pairself @{code int_of_integer};
+val mk_poly_Bound = @{code poly.Bound} o @{code nat_of_integer};
+val mk_Bound = @{code Bound} o @{code nat_of_integer};
+
 val dest_num = snd o HOLogic.dest_number;
 
 fun try_dest_num t = SOME ((snd o HOLogic.dest_number) t)
@@ -2812,19 +2816,19 @@
   | num_of_term ps (Const (@{const_name Groups.plus}, _) $ a $ b) = @{code poly.Add} (num_of_term ps a, num_of_term ps b)
   | num_of_term ps (Const (@{const_name Groups.minus}, _) $ a $ b) = @{code poly.Sub} (num_of_term ps a, num_of_term ps b)
   | num_of_term ps (Const (@{const_name Groups.times}, _) $ a $ b) = @{code poly.Mul} (num_of_term ps a, num_of_term ps b)
-  | num_of_term ps (Const (@{const_name Power.power}, _) $ a $ n) = @{code poly.Pw} (num_of_term ps a, dest_nat n)
-  | num_of_term ps (Const (@{const_name Fields.divide}, _) $ a $ b) = @{code poly.C} (dest_num a, dest_num b)
+  | num_of_term ps (Const (@{const_name Power.power}, _) $ a $ n) = @{code poly.Pw} (num_of_term ps a, @{code nat_of_integer} (dest_nat n))
+  | num_of_term ps (Const (@{const_name Fields.divide}, _) $ a $ b) = mk_C (dest_num a, dest_num b)
   | num_of_term ps t = (case try_dest_num t
-     of SOME k => @{code poly.C} (k, 1)
-      | NONE => @{code poly.Bound} (the_index ps t));
+     of SOME k => mk_C (k, 1)
+      | NONE => mk_poly_Bound (the_index ps t));
 
 fun tm_of_term fs ps (Const(@{const_name Groups.uminus}, _) $ t) = @{code Neg} (tm_of_term fs ps t)
   | tm_of_term fs ps (Const(@{const_name Groups.plus}, _) $ a $ b) = @{code Add} (tm_of_term fs ps a, tm_of_term fs ps b)
   | tm_of_term fs ps (Const(@{const_name Groups.minus}, _) $ a $ b) = @{code Sub} (tm_of_term fs ps a, tm_of_term fs ps b)
   | tm_of_term fs ps (Const(@{const_name Groups.times}, _) $ a $ b) = @{code Mul} (num_of_term ps a, tm_of_term fs ps b)
   | tm_of_term fs ps t = (@{code CP} (num_of_term ps t) 
-      handle TERM _ => @{code Bound} (the_index fs t)
-           | General.Subscript => @{code Bound} (the_index fs t));
+      handle TERM _ => mk_Bound (the_index fs t)
+           | General.Subscript => mk_Bound (the_index fs t));
 
 fun fm_of_term fs ps @{term True} = @{code T}
   | fm_of_term fs ps @{term False} = @{code F}
@@ -2850,21 +2854,25 @@
   | fm_of_term fs ps _ = error "fm_of_term";
 
 fun term_of_num T ps (@{code poly.C} (a, b)) = 
-    (if b = 1 then HOLogic.mk_number T a
-     else if b = 0 then Const (@{const_name Groups.zero}, T)
-     else Const (@{const_name Fields.divide}, binopT T) $ HOLogic.mk_number T a $ HOLogic.mk_number T b)
-  | term_of_num T ps (@{code poly.Bound} i) = nth ps i
+      let
+        val (c, d) = pairself (@{code integer_of_int}) (a, b)
+      in
+        (if d = 1 then HOLogic.mk_number T c
+        else if d = 0 then Const (@{const_name Groups.zero}, T)
+        else Const (@{const_name Fields.divide}, binopT T) $ HOLogic.mk_number T c $ HOLogic.mk_number T d)
+      end
+  | term_of_num T ps (@{code poly.Bound} i) = nth ps (@{code integer_of_nat} i)
   | term_of_num T ps (@{code poly.Add} (a, b)) = Const (@{const_name Groups.plus}, binopT T) $ term_of_num T ps a $ term_of_num T ps b
   | term_of_num T ps (@{code poly.Mul} (a, b)) = Const (@{const_name Groups.times}, binopT T) $ term_of_num T ps a $ term_of_num T ps b
   | term_of_num T ps (@{code poly.Sub} (a, b)) = Const (@{const_name Groups.minus}, binopT T) $ term_of_num T ps a $ term_of_num T ps b
   | term_of_num T ps (@{code poly.Neg} a) = Const (@{const_name Groups.uminus}, T --> T) $ term_of_num T ps a
-  | term_of_num T ps (@{code poly.Pw} (a, n)) =
-      Const (@{const_name Power.power}, T --> @{typ nat} --> T) $ term_of_num T ps a $ HOLogic.mk_number HOLogic.natT n
+  | term_of_num T ps (@{code poly.Pw} (a, n)) = Const (@{const_name Power.power},
+      T --> @{typ nat} --> T) $ term_of_num T ps a $ HOLogic.mk_number HOLogic.natT (@{code integer_of_nat} n)
   | term_of_num T ps (@{code poly.CN} (c, n, p)) =
       term_of_num T ps (@{code poly.Add} (c, @{code poly.Mul} (@{code poly.Bound} n, p)));
 
 fun term_of_tm T fs ps (@{code CP} p) = term_of_num T ps p
-  | term_of_tm T fs ps (@{code Bound} i) = nth fs i
+  | term_of_tm T fs ps (@{code Bound} i) = nth fs (@{code integer_of_nat} i)
   | term_of_tm T fs ps (@{code Add} (a, b)) = Const (@{const_name Groups.plus}, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b
   | term_of_tm T fs ps (@{code Mul} (a, b)) = Const (@{const_name Groups.times}, binopT T) $ term_of_num T ps a $ term_of_tm T fs ps b
   | term_of_tm T fs ps (@{code Sub} (a, b)) = Const (@{const_name Groups.minus}, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b
@@ -2993,3 +3001,4 @@
 *)
 end
 
+