diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/Lambda_F_T.thy
--- a/Nominal/Ex/Lambda_F_T.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Lambda_F_T.thy	Mon May 19 12:45:26 2014 +0100
@@ -47,7 +47,7 @@
     and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l"
 begin
 
-nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")
+nominal_function (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")
   f
 where
   "f (Var x) l = f1 x l"
@@ -157,7 +157,7 @@
     \<Longrightarrow> P"
 sorry
 
-nominal_primrec
+nominal_function
   g
 where
   "(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t"