--- a/src/HOL/ex/coopereif.ML Thu Jul 26 21:49:53 2007 +0200
+++ b/src/HOL/ex/coopereif.ML Thu Jul 26 21:49:55 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
- | Cx (i, t') => term_of_i vs (Add (Mul (i, Bound (nat 0)), t'));
+ | Cn (n,i, t') => term_of_i vs (Add (Mul (i, Bound (nat n)), t'));
fun term_of_qf ps vs t = case t
of T => HOLogic.true_const