diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Classical.thy	Mon May 19 12:45:26 2014 +0100
@@ -47,7 +47,7 @@
 thm trm.supp
 thm trm.supp[simplified]
 
-nominal_primrec 
+nominal_function 
   crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
 where
   "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" 
@@ -252,7 +252,7 @@
 termination (eqvt)
   by lexicographic_order
 
-nominal_primrec 
+nominal_function 
   nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm"      ("_[_\<turnstile>n>_]" [100,100,100] 100) 
 where
   "(Ax x a)[u\<turnstile>n>v] = (if x=u then Ax v a else Ax x a)" 
@@ -449,7 +449,7 @@
 thm crename.eqvt nrename.eqvt
 
 
-nominal_primrec 
+nominal_function 
   substn :: "trm \<Rightarrow> name   \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100) 
 where
   "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)"