--- a/Nominal/Ex/CR.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/CR.thy	Mon May 19 12:45:26 2014 +0100
@@ -10,7 +10,7 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
-nominal_primrec
+nominal_function
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
 where
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"