--- a/Nominal/Ex/Pi.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Pi.thy	Mon May 19 12:45:26 2014 +0100
@@ -27,7 +27,7 @@
     by(auto)
 qed
 
-nominal_primrec
+nominal_function
   subst_name_list :: "name \<Rightarrow> (name \<times> name) list \<Rightarrow> name"
 where
   "subst_name_list a [] = a"
@@ -143,7 +143,7 @@
   shows "(p \<bullet> (Sum_Type.projl (Sum_Type.projr f))) = Sum_Type.projl (Sum_Type.projr (p \<bullet> f))"
 using a by auto
 
-nominal_primrec (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
+nominal_function (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
   subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix"  ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and
   subsList_mix  :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix"          ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and
   subs_mix      :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix"                      ("_[_::=\<onesuperior>_]" [100, 100, 100] 100)
@@ -568,4 +568,4 @@
 nominal_inductive fresh_list_mix
   done
 
-end
\ No newline at end of file
+end