diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/SFT/Consts.thy
--- a/Nominal/Ex/SFT/Consts.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/SFT/Consts.thy	Mon May 19 12:45:26 2014 +0100
@@ -71,7 +71,7 @@
   "p \<bullet> VAR = VAR" "p \<bullet> APP = APP" "p \<bullet> Abs = Abs"
   by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def)
 
-nominal_primrec
+nominal_function
   Numeral :: "lam \<Rightarrow> lam" ("\<lbrace>_\<rbrace>" 1000)
 where
   "\<lbrace>Var x\<rbrace> = VAR \<cdot> (Var x)"
@@ -128,7 +128,7 @@
 lemma app_lst_rev_eq_iff: "app_lst n (rev M) = app_lst n (rev N) \<Longrightarrow> M = N"
   by (drule app_lst_eq_iff) simp
 
-nominal_primrec
+nominal_function
   Ltgt :: "lam list \<Rightarrow> lam" ("\<guillemotleft>_\<guillemotright>" 1000)
 where
   [simp del]: "atom x \<sharp> l \<Longrightarrow> \<guillemotleft>l\<guillemotright> = \<integral>x. (app_lst x (rev l))"