# HG changeset patch # User chaieb # Date 1185545066 -7200 # Node ID 467e77e4e276d396a07995f1ddc57296cc52a275 # Parent 393dd64d0d04d65d53e3a8aeb4bffcea92d0d486 no 'nat' is needed for Bound in reification diff -r 393dd64d0d04 -r 467e77e4e276 src/HOL/ex/coopereif.ML --- a/src/HOL/ex/coopereif.ML Fri Jul 27 10:18:56 2007 +0200 +++ b/src/HOL/ex/coopereif.ML Fri Jul 27 16:04:26 2007 +0200 @@ -92,7 +92,7 @@ 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