diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/TypeSchemes1.thy
--- a/Nominal/Ex/TypeSchemes1.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/TypeSchemes1.thy	Mon May 19 12:45:26 2014 +0100
@@ -75,7 +75,7 @@
   shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
   by (induct Ts T rule: lookup.induct) (simp_all)
 
-nominal_primrec
+nominal_function
   subst  :: "Subst \<Rightarrow> ty \<Rightarrow> ty" ("_<_>" [100,60] 120)
 where
   "\<theta><Var X> = lookup \<theta> X"
@@ -114,7 +114,7 @@
   unfolding eqvt_def 
   by (simp add: permute_fun_def subst.eqvt)
  
-nominal_primrec
+nominal_function
   substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120)
 where
   "fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"
@@ -272,7 +272,7 @@
 apply(simp add: fresh_def supp_perm)
 done
 
-nominal_primrec
+nominal_function
   generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _")
 where
   "atom ` (fset Xs) \<sharp>* T \<Longrightarrow>  
@@ -399,7 +399,7 @@
 apply(simp add: compose_ty[symmetric] subst_id2 compose_Dom)
 done
 
-nominal_primrec
+nominal_function
   ftv  :: "ty \<Rightarrow> name fset"
 where
   "ftv (Var X) = {|X|}"