diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/Local_Contexts.thy
--- a/Nominal/Ex/Local_Contexts.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Local_Contexts.thy	Mon May 19 12:45:26 2014 +0100
@@ -29,7 +29,7 @@
 lemma atom_image_set_eq_supp: "atom ` set xs = supp xs"
 by (metis image_set set_map_atom_eq_supp)
 
-nominal_primrec (in name_subst)
+nominal_function (in name_subst)
   subst :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [120,120,120] 120)
 where
   "(Var x)[xs::=t] = name_subst x xs t"