1.1 --- a/doc-src/TutorialI/Datatype/Nested.thy	Thu May 29 13:27:13 2008 +0200
     1.2 +++ b/doc-src/TutorialI/Datatype/Nested.thy	Thu May 29 22:45:33 2008 +0200
     1.3 @@ -43,17 +43,16 @@
     1.4  lists, we need to define two substitution functions simultaneously:
     1.5  *}
     1.6  
     1.7 -consts
     1.8 -subst :: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term      \<Rightarrow> ('v,'f)term"
     1.9 -substs:: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term list \<Rightarrow> ('v,'f)term list";
    1.10 +primrec
    1.11 +subst :: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term      \<Rightarrow> ('v,'f)term" and
    1.12 +substs:: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term list \<Rightarrow> ('v,'f)term list"
    1.13 +where
    1.14 +"subst s (Var x) = s x" |
    1.15 +  subst_App:
    1.16 +"subst s (App f ts) = App f (substs s ts)" |
    1.17  
    1.18 -primrec
    1.19 -  "subst s (Var x) = s x"
    1.20 -  subst_App:
    1.21 -  "subst s (App f ts) = App f (substs s ts)"
    1.22 -
    1.23 -  "substs s [] = []"
    1.24 -  "substs s (t # ts) = subst s t # substs s ts";
    1.25 +"substs s [] = []" |
    1.26 +"substs s (t # ts) = subst s t # substs s ts"
    1.27  
    1.28  text{*\noindent
    1.29  Individual equations in a \commdx{primrec} definition may be