--- a/Nominal/Ex/CPS/Lt.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/CPS/Lt.thy	Mon May 19 12:45:26 2014 +0100
@@ -10,7 +10,7 @@
   | App lt lt         (infixl "$$" 100)
   | Lam x::"name" t::"lt"  binds  x in t
 
-nominal_primrec
+nominal_function
   subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt"  ("_ [_ ::= _]" [90, 90, 90] 90)
 where
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
@@ -44,7 +44,7 @@
   by (nominal_induct M avoiding: x V rule: lt.strong_induct)
      (auto simp add: lt.supp supp_at_base, blast, blast)
 
-nominal_primrec
+nominal_function
   isValue:: "lt => bool"
 where
   "isValue (Var x) = True"