--- a/Nominal/Ex/SubstNoFcb.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/SubstNoFcb.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 lam_rec ::
+nominal_function lam_rec ::
   "(name \<Rightarrow> 'a :: pt) \<Rightarrow> (lam \<Rightarrow> lam \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> lam \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b :: fs \<Rightarrow> lam \<Rightarrow> 'a"
 where
   "lam_rec fv fa fl fd P (Var n) = fv n"
@@ -49,7 +49,7 @@
   using Abs1_eq_iff lam.eq_iff apply metis
   done
 
-nominal_primrec substr where
+nominal_function substr where
 [simp del]: "substr l y s = lam_rec
   (%x. if x = y then s else (Var x))
   (%t1 t2. App (substr t1 y s) (substr t2 y s))