src/HOL/ex/coopereif.ML

   | Add (t1, t2) => @{term "op +:: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
   | Sub (t1, t2) => Const (@{const_name "HOL.minus"}, HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $
       term_of_i vs t1 $ term_of_i vs t2
   | Mul (i, t2) => Const (@{const_name "HOL.times"}, HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $
       HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
-  | Cn (n,i, t') => term_of_i vs (Add (Mul (i, Bound (nat n)), t'));
+  | Cn (n,i, t') => term_of_i vs (Add (Mul (i, Bound n), t'));
 
 fun term_of_qf ps vs t = case t
  of T => HOLogic.true_const 
   | F => HOLogic.false_const
   | Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}