diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/CPS/CPS1_Plotkin.thy
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Mon May 19 12:45:26 2014 +0100
@@ -3,7 +3,7 @@
 imports Lt
 begin
 
-nominal_primrec
+nominal_function
   CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250)
 where
   "atom k \<sharp> x \<Longrightarrow> (x~)* = (Lam k ((k~) $$ (x~)))"
@@ -74,7 +74,7 @@
 lemma [simp]: "x \<sharp> M* = x \<sharp> M"
   unfolding fresh_def by simp
 
-nominal_primrec
+nominal_function
   convert:: "lt => lt" ("_+" [250] 250)
 where
   "(Var x)+ = Var x"
@@ -104,7 +104,7 @@
   shows "isValue (p \<bullet> (M::lt)) = isValue M"
   by (nominal_induct M rule: lt.strong_induct) auto
 
-nominal_primrec
+nominal_function
   Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt"       (infixl ";" 100)
 where
   "Kapply (Lam x M) K = K $$ (Lam x M)+"