diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/Exec/Lambda_Exec.thy
--- a/Nominal/Ex/Exec/Lambda_Exec.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Exec/Lambda_Exec.thy	Mon May 19 12:45:26 2014 +0100
@@ -7,7 +7,7 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
-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))"
@@ -122,7 +122,7 @@
   shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
   by (induct xs arbitrary: n) (simp_all add: permute_pure)
 
-nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
+nominal_function (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
   lam_ln_aux :: "lam \<Rightarrow> name list \<Rightarrow> ln"
 where
   "lam_ln_aux (Var x) xs = lookup xs 0 x"
@@ -164,7 +164,7 @@
   apply simp_all
   done
 
-nominal_primrec
+nominal_function
   ln_lam_aux :: "ln \<Rightarrow> name list \<Rightarrow> lam"
 where
   "ln_lam_aux (LNBnd n) ns = (nth_or_def (map Var ns) n (Lam [x]. Var x))"
@@ -321,7 +321,7 @@
   "atom y \<sharp> subst_ln_nat t x n \<longleftrightarrow> y = x \<or> atom y \<sharp> t"
   unfolding fresh_def supp_subst_ln_nat by auto
 
-nominal_primrec
+nominal_function
   lam_ln_ex :: "lam \<Rightarrow> ln"
 where
   "lam_ln_ex (Var x) = LNVar x"