diff -r 08c3ef07cef7 -r 5ebd327ffb96 Tutorial/Lambda.thy --- a/Tutorial/Lambda.thy Mon May 19 11:19:48 2014 +0100 +++ b/Tutorial/Lambda.thy Mon May 19 12:45:26 2014 +0100 @@ -32,7 +32,7 @@ subsection {* Height Function *} -nominal_primrec +nominal_function height :: "lam \ int" where "height (Var x) = 1" @@ -53,7 +53,7 @@ subsection {* Capture-Avoiding Substitution *} -nominal_primrec +nominal_function subst :: "lam \ name \ lam \ lam" ("_ [_ ::= _]" [90,90,90] 90) where "(Var x)[y ::= s] = (if x = y then s else (Var x))"