--- 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 \<Rightarrow> int"
 where
   "height (Var x) = 1"
@@ -53,7 +53,7 @@
 
 subsection {* Capture-Avoiding Substitution *}
 
-nominal_primrec
+nominal_function
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90,90,90] 90)
 where
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"