Dear Leonor and Ricardo,

we are trying to define a function that uses nested primitive recursion
but we get the error below. We reproduce the error by using

`the example in the tutorial where the recursion is inside a list and
``inside
`a tuple (this seems to be the problem).

`Primrec requires that you define a separate function for the pair. The
``following works:
`
consts
subst :: "('v => ('v,'f)term) => ('v,'f)term => ('v,'f)term"

` substs:: "('v => ('v,'f)term) => (('v,'f)term × nat) list =>
``(('v,'f)term × nat) list"
` substp:: "('v => ('v,'f)term) => ('v,'f)term × nat => ('v,'f)term × nat"
primrec
"subst s (Var x) = s x"
subst_App:
"subst s (App f ts) = App f (substs s ts)"
"substs s [] = []"
"substp s (t,n) = (subst s t, n)"
"substs s (t # ts) = (substp s t # substs s ts)"

`Instead of primrec, you could also use function/fun, which is more
``liberal. For example:
`

`lemma term_size[simp]: "(a, b) : set ts ==> size a < Suc
``term_nat_x_list_size ts)"
`by (induct ts) auto
fun
subst :: "('v => ('v,'f)term) => ('v,'f)term => ('v,'f)term"
where
"subst s (Var x) = s x"
| "subst s (App f ts) = App f (map (%(t,n). (subst s t, n)) ts)"

`The funny lemma about size is still required in Isabelle 2007, but will
``be unnecessary in the next version.
`
Alex