diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/NBE.thy
--- a/Nominal/Ex/NBE.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/NBE.thy	Mon May 19 12:45:26 2014 +0100
@@ -88,7 +88,7 @@
 using assms by (auto simp add: fresh_star_def)
   
 
-nominal_primrec  (invariant "\<lambda>x y. case x of Inl (x1, y1) \<Rightarrow> 
+nominal_function  (invariant "\<lambda>x y. case x of Inl (x1, y1) \<Rightarrow> 
   supp y \<subseteq> (supp y1 - set (bn x1)) \<union> (fv_bn x1) | Inr (x2, y2) \<Rightarrow> supp y \<subseteq> supp x2 \<union> supp y2")
   evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
   evals_aux :: "sem \<Rightarrow> sem \<Rightarrow> sem"
@@ -346,7 +346,7 @@
 done
 
 
-nominal_primrec
+nominal_function
   reify :: "sem \<Rightarrow> lam" and
   reifyn :: "neu \<Rightarrow> lam"
 where
@@ -543,4 +543,4 @@
 where
   "normalize t = reify (eval t)"
 
-end
\ No newline at end of file
+end