--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Mon May 19 12:45:26 2014 +0100
@@ -9,7 +9,7 @@
 | CArg lt cpsctxt
 | CAbs x::name c::cpsctxt binds x in c
 
-nominal_primrec
+nominal_function
   fill   :: "cpsctxt \<Rightarrow> lt \<Rightarrow> lt"         ("_<_>" [200, 200] 100)
 where
   fill_hole : "Hole<M> = M"
@@ -34,7 +34,7 @@
 
 termination (eqvt) by lexicographic_order
 
-nominal_primrec
+nominal_function
   ccomp :: "cpsctxt => cpsctxt => cpsctxt"
 where
   "ccomp Hole C  = C"
@@ -59,7 +59,7 @@
 
 termination (eqvt) by lexicographic_order
 
-nominal_primrec
+nominal_function
     CPSv :: "lt => lt"
 and CPS :: "lt => cpsctxt" where
   "CPSv (Var x) = x~"