--- a/Nominal/Ex/AuxNoFCB.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/AuxNoFCB.thy	Mon May 19 12:45:26 2014 +0100
@@ -7,7 +7,7 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
-nominal_primrec lookup where
+nominal_function lookup where
   "lookup (n :: name) m [] \<longleftrightarrow> (n = m)"
 | "lookup n m ((hn, hm) # t) \<longleftrightarrow>
      (n, m) = (hn, hm) \<or> (n \<noteq> hn \<and> m \<noteq> hm \<and> lookup n m t)"
@@ -17,7 +17,7 @@
 
 termination (eqvt) by lexicographic_order
 
-nominal_primrec lam2_rec where
+nominal_function lam2_rec where
   "lam2_rec faa fll xs (Var n) (Var m) = lookup n m xs"
 | "lam2_rec faa fll xs (Var n) (App l r) = False"
 | "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False"
@@ -97,7 +97,7 @@
   apply (subst lam2_rec.simps(10)) apply (simp_all add: fresh_star_def)
   done
 
-nominal_primrec aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool"
+nominal_function aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool"
   where
 [simp del]: "aux l r xs = lam2_rec
   (%t1 t2 t3 t4. (aux t1 t3 xs) \<and> (aux t2 t4 xs))
@@ -204,7 +204,7 @@
   apply lexicographic_order
   done
 
-nominal_primrec swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where
+nominal_function swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where
   "swapequal l r [] \<longleftrightarrow> l = r"
 | "atom x \<sharp> (l, r, hl, hr, t) \<Longrightarrow>
     swapequal l r ((hl, hr) # t) \<longleftrightarrow> swapequal ((hl \<leftrightarrow> x) \<bullet> l) ((hr \<leftrightarrow> x) \<bullet> r) t"