# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1400499926 -3600
# Node ID 5ebd327ffb96d118e923d20540020d236216b971
# Parent  08c3ef07cef78e3ae595b4d2ec698f7751330543
changed nominal_primrec into the more appropriate nominal_function

diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/AuxNoFCB.thy
--- 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"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/Beta.thy
--- a/Nominal/Ex/Beta.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Beta.thy	Mon May 19 12:45:26 2014 +0100
@@ -14,7 +14,7 @@
 
 section {* capture-avoiding substitution *}
 
-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))"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/CPS/CPS1_Plotkin.thy
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Mon May 19 12:45:26 2014 +0100
@@ -3,7 +3,7 @@
 imports Lt
 begin
 
-nominal_primrec
+nominal_function
   CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250)
 where
   "atom k \<sharp> x \<Longrightarrow> (x~)* = (Lam k ((k~) $$ (x~)))"
@@ -74,7 +74,7 @@
 lemma [simp]: "x \<sharp> M* = x \<sharp> M"
   unfolding fresh_def by simp
 
-nominal_primrec
+nominal_function
   convert:: "lt => lt" ("_+" [250] 250)
 where
   "(Var x)+ = Var x"
@@ -104,7 +104,7 @@
   shows "isValue (p \<bullet> (M::lt)) = isValue M"
   by (nominal_induct M rule: lt.strong_induct) auto
 
-nominal_primrec
+nominal_function
   Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt"       (infixl ";" 100)
 where
   "Kapply (Lam x M) K = K $$ (Lam x M)+"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/CPS/CPS2_DanvyNielsen.thy
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Mon May 19 12:45:26 2014 +0100
@@ -9,7 +9,7 @@
 | CArg lt cpsctxt
 | CAbs x::name c::cpsctxt binds x in c
 
-nominal_primrec
+nominal_function
   fill   :: "cpsctxt \<Rightarrow> lt \<Rightarrow> lt"         ("_<_>" [200, 200] 100)
 where
   fill_hole : "Hole<M> = M"
@@ -34,7 +34,7 @@
 
 termination (eqvt) by lexicographic_order
 
-nominal_primrec
+nominal_function
   ccomp :: "cpsctxt => cpsctxt => cpsctxt"
 where
   "ccomp Hole C  = C"
@@ -59,7 +59,7 @@
 
 termination (eqvt) by lexicographic_order
 
-nominal_primrec
+nominal_function
     CPSv :: "lt => lt"
 and CPS :: "lt => cpsctxt" where
   "CPSv (Var x) = x~"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/CPS/CPS3_DanvyFilinski.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Mon May 19 12:45:26 2014 +0100
@@ -1,7 +1,7 @@
 header {* CPS transformation of Danvy and Filinski *}
 theory CPS3_DanvyFilinski imports Lt begin
 
-nominal_primrec
+nominal_function
   CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_"  [100,100] 100)
 and
   CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Mon May 19 12:45:26 2014 +0100
@@ -3,7 +3,7 @@
 imports Lt 
 begin
 
-nominal_primrec
+nominal_function
   CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_"  [100,100] 100)
 and
   CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/CPS/Lt.thy
--- a/Nominal/Ex/CPS/Lt.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/CPS/Lt.thy	Mon May 19 12:45:26 2014 +0100
@@ -10,7 +10,7 @@
   | App lt lt         (infixl "$$" 100)
   | Lam x::"name" t::"lt"  binds  x in t
 
-nominal_primrec
+nominal_function
   subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt"  ("_ [_ ::= _]" [90, 90, 90] 90)
 where
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
@@ -44,7 +44,7 @@
   by (nominal_induct M avoiding: x V rule: lt.strong_induct)
      (auto simp add: lt.supp supp_at_base, blast, blast)
 
-nominal_primrec
+nominal_function
   isValue:: "lt => bool"
 where
   "isValue (Var x) = True"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/CR.thy
--- 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))"
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)" 
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/Exec/Lambda_Exec.thy
--- a/Nominal/Ex/Exec/Lambda_Exec.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Exec/Lambda_Exec.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
+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))"
@@ -122,7 +122,7 @@
   shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
   by (induct xs arbitrary: n) (simp_all add: permute_pure)
 
-nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
+nominal_function (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
   lam_ln_aux :: "lam \<Rightarrow> name list \<Rightarrow> ln"
 where
   "lam_ln_aux (Var x) xs = lookup xs 0 x"
@@ -164,7 +164,7 @@
   apply simp_all
   done
 
-nominal_primrec
+nominal_function
   ln_lam_aux :: "ln \<Rightarrow> name list \<Rightarrow> lam"
 where
   "ln_lam_aux (LNBnd n) ns = (nth_or_def (map Var ns) n (Lam [x]. Var x))"
@@ -321,7 +321,7 @@
   "atom y \<sharp> subst_ln_nat t x n \<longleftrightarrow> y = x \<or> atom y \<sharp> t"
   unfolding fresh_def supp_subst_ln_nat by auto
 
-nominal_primrec
+nominal_function
   lam_ln_ex :: "lam \<Rightarrow> ln"
 where
   "lam_ln_ex (Var x) = LNVar x"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/FiniteType.thy
--- a/Nominal/Ex/FiniteType.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/FiniteType.thy	Mon May 19 12:45:26 2014 +0100
@@ -16,4 +16,4 @@
 
 
 
-end
\ No newline at end of file
+end
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/LamTest.thy
--- a/Nominal/Ex/LamTest.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LamTest.thy	Mon May 19 12:45:26 2014 +0100
@@ -1507,7 +1507,7 @@
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.local_theory_to_proof "nominal_primrec" "define recursive functions for nominal types"
+  Outer_Syntax.local_theory_to_proof "nominal_function" "define recursive functions for nominal types"
   Keyword.thy_goal
   (function_parser default_config
      >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
@@ -1545,7 +1545,7 @@
   shows "(a \<rightleftharpoons> c) \<bullet> x = (b \<rightleftharpoons> c) \<bullet> y"
 using assms by (simp add: swap_fresh_fresh)
 
-nominal_primrec
+nominal_function
   depth :: "lam \<Rightarrow> nat"
 where
   "depth (Var x) = 1"
@@ -1566,7 +1566,7 @@
   shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
 by (induct xs) (auto)
 
-nominal_primrec 
+nominal_function 
   frees_lst :: "lam \<Rightarrow> atom list"
 where
   "frees_lst (Var x) = [atom x]"
@@ -1585,7 +1585,7 @@
 apply(clarify)
 oops
 
-nominal_primrec
+nominal_function
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
 where
   "(Var x)[y ::= s] = (if x=y then s else (Var x))"
@@ -1608,7 +1608,7 @@
 
 
 
-nominal_primrec
+nominal_function
   depth :: "lam \<Rightarrow> nat"
 where
   "depth (Var x) = 1"
@@ -1665,7 +1665,7 @@
   shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
 by (induct xs) (auto)
 
-nominal_primrec 
+nominal_function 
   frees_lst :: "lam \<Rightarrow> atom list"
 where
   "frees_lst (Var x) = [atom x]"
@@ -1687,7 +1687,7 @@
 apply(rule_tac p="p" in supp_perm_eq)
 oops
 
-nominal_primrec 
+nominal_function 
   frees :: "lam \<Rightarrow> name set"
 where
   "frees (Var x) = {x}"
@@ -1771,7 +1771,7 @@
 apply(simp add: set_eqvt)
 sorry
 
-nominal_primrec
+nominal_function
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
 where
   "(Var x)[y ::= s] = (if x=y then s else (Var x))"
@@ -1822,7 +1822,7 @@
 
 
 
-nominal_primrec
+nominal_function
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
 where
   "(Var x)[y ::= s] = (if x=y then s else (Var x))"
@@ -1874,7 +1874,7 @@
 done
 
 (* this should not work *)
-nominal_primrec 
+nominal_function 
   bnds :: "lam \<Rightarrow> name set"
 where
   "bnds (Var x) = {}"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Lambda.thy	Mon May 19 12:45:26 2014 +0100
@@ -72,7 +72,7 @@
 
 section {* Simple examples from Norrish 2004 *}
 
-nominal_primrec 
+nominal_function 
   is_app :: "lam \<Rightarrow> bool"
 where
   "is_app (Var x) = False"
@@ -93,7 +93,7 @@
 
 thm eqvts
 
-nominal_primrec 
+nominal_function 
   rator :: "lam \<Rightarrow> lam option"
 where
   "rator (Var x) = None"
@@ -108,7 +108,7 @@
 
 termination (eqvt) by lexicographic_order
 
-nominal_primrec 
+nominal_function 
   rand :: "lam \<Rightarrow> lam option"
 where
   "rand (Var x) = None"
@@ -123,7 +123,7 @@
 
 termination (eqvt) by lexicographic_order
 
-nominal_primrec 
+nominal_function 
   is_eta_nf :: "lam \<Rightarrow> bool"
 where
   "is_eta_nf (Var x) = True"
@@ -154,7 +154,7 @@
 apply(simp_all)
 done
 
-nominal_primrec 
+nominal_function 
   var_pos :: "name \<Rightarrow> lam \<Rightarrow> (path list) set"
 where
   "var_pos y (Var x) = (if y = x then {[]} else {})"
@@ -200,7 +200,7 @@
 
 text {* strange substitution operation *}
 
-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))"
@@ -234,7 +234,7 @@
 
 text {* first returns an atom list *}
 
-nominal_primrec 
+nominal_function 
   frees_lst :: "lam \<Rightarrow> atom list"
 where
   "frees_lst (Var x) = [atom x]"
@@ -260,7 +260,7 @@
 
 text {* second returns an atom set - therefore needs an invariant *}
 
-nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
+nominal_function (invariant "\<lambda>x (y::atom set). finite y")
   frees_set :: "lam \<Rightarrow> atom set"
 where
   "frees_set (Var x) = {atom x}"
@@ -288,7 +288,7 @@
 
 section {* height function *}
 
-nominal_primrec
+nominal_function
   height :: "lam \<Rightarrow> int"
 where
   "height (Var x) = 1"
@@ -311,7 +311,7 @@
   
 section {* capture-avoiding substitution *}
 
-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))"
@@ -501,7 +501,7 @@
 
 text {* Function that translates lambda-terms into locally nameless terms *}
 
-nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
+nominal_function (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
   trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
 where
   "trans (Var x) xs = lookup xs 0 x"
@@ -536,7 +536,7 @@
 
 text {* count the occurences of lambdas in a term *}
 
-nominal_primrec
+nominal_function
   cntlams :: "lam  \<Rightarrow> nat"
 where
   "cntlams (Var x) = 0"
@@ -563,7 +563,7 @@
 
 text {* count the bound-variable occurences in a lambda-term *}
 
-nominal_primrec
+nominal_function
   cntbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat"
 where
   "cntbvs (Var x) xs = (if x \<in> set xs then 1 else 0)"
@@ -621,7 +621,7 @@
   "(p \<bullet> vindex l v n) = vindex (p \<bullet> l) (p \<bullet> v) (p \<bullet> n)"
   by (induct l arbitrary: n) (simp_all add: permute_pure)
 
-nominal_primrec
+nominal_function
   transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option"
 where
   "transdb (Var x) l = vindex l x 0"
@@ -679,7 +679,7 @@
   by (induct t x s rule: subst.induct) (auto simp add: lam.supp  fresh_at_base)
 
 (* function that evaluates a lambda term *)
-nominal_primrec
+nominal_function
    eval :: "lam \<Rightarrow> lam" and
    apply_subst :: "lam \<Rightarrow> lam \<Rightarrow> lam"
 where
@@ -734,7 +734,7 @@
 
 
 text {* TODO: eqvt_at for the other side *}
-nominal_primrec q where
+nominal_function q where
   "atom c \<sharp> (x, M) \<Longrightarrow> q (Lam [x]. M) (N :: lam) = Lam [x]. (Lam [c]. (App M (q (Var c) N)))"
 | "q (Var x) N = Var x"
 | "q (App l r) N = App l r"
@@ -757,7 +757,7 @@
 
 text {* Working Examples *}
 
-nominal_primrec
+nominal_function
   map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam"
 where
   "eqvt f \<Longrightarrow> map_term f (Var x) = f (Var x)"
@@ -821,7 +821,7 @@
 *)
 
 (*
-nominal_primrec
+nominal_function
   trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
 where
   "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n::nat. Some (DBVar n)))"
@@ -831,7 +831,7 @@
 oops
 *)
 
-nominal_primrec
+nominal_function
   CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
 where
   "CPS (Var x) k = Var x"
@@ -839,7 +839,7 @@
 oops
 
 consts b :: name
-nominal_primrec
+nominal_function
   Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
 where
   "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
@@ -871,7 +871,7 @@
 
 
 
-nominal_primrec  (invariant "\<lambda>(_, _, xs) y. atom ` fst ` set xs \<sharp>* y \<and> atom ` snd ` set xs \<sharp>* y")
+nominal_function  (invariant "\<lambda>(_, _, xs) y. atom ` fst ` set xs \<sharp>* y \<and> atom ` snd ` set xs \<sharp>* y")
   aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool"
 where
   "aux (Var x) (Var y) xs = ((x, y) \<in> set xs)"
@@ -919,7 +919,7 @@
      \<longleftrightarrow> [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)"
   by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff assms fresh_Pair)
 
-nominal_primrec
+nominal_function
   aux2 :: "lam \<Rightarrow> lam \<Rightarrow> bool"
 where
   "aux2 (Var x) (Var y) = (x = y)"
@@ -961,7 +961,7 @@
 consts P :: "lam \<Rightarrow> bool"
 
 (*
-nominal_primrec  
+nominal_function  
   A :: "lam => lam"
 where  
   "A (App M N) = (if (True \<or> P M) then (A M) else (A N))"
@@ -969,7 +969,7 @@
 | "A (App M N) = (if True then M else A N)"
 oops
 
-nominal_primrec  
+nominal_function  
   C :: "lam => lam"
 where  
   "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))"
@@ -977,7 +977,7 @@
 | "C (App M N) = (if True then M else C N)"
 oops
 
-nominal_primrec  
+nominal_function  
   A :: "lam => lam"
 where  
   "A (Lam [x].M) = (Lam [x].M)"
@@ -985,7 +985,7 @@
 | "A (App M N) = (if True then M else A N)"
 oops
 
-nominal_primrec  
+nominal_function  
   B :: "lam => lam"
 where  
   "B (Lam [x].M) = (Lam [x].M)"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/Lambda_F_T.thy
--- a/Nominal/Ex/Lambda_F_T.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Lambda_F_T.thy	Mon May 19 12:45:26 2014 +0100
@@ -47,7 +47,7 @@
     and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l"
 begin
 
-nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")
+nominal_function (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")
   f
 where
   "f (Var x) l = f1 x l"
@@ -157,7 +157,7 @@
     \<Longrightarrow> P"
 sorry
 
-nominal_primrec
+nominal_function
   g
 where
   "(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/Lambda_F_T_FCB2.thy
--- a/Nominal/Ex/Lambda_F_T_FCB2.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Lambda_F_T_FCB2.thy	Mon May 19 12:45:26 2014 +0100
@@ -133,7 +133,7 @@
     and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l"
 begin
 
-nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")
+nominal_function (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")
   f
 where
   "f (Var x) l = f1 x l"
@@ -244,7 +244,7 @@
     \<Longrightarrow> P"
 sorry
 
-nominal_primrec
+nominal_function
   g
 where
   "(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Let.thy	Mon May 19 12:45:26 2014 +0100
@@ -107,7 +107,7 @@
   apply simp_all
   done
 
-nominal_primrec
+nominal_function
     height_trm :: "trm \<Rightarrow> nat"
 where
   "height_trm (Var x) = 1"
@@ -160,7 +160,7 @@
   apply (simp_all add: trm_assn.bn_defs)
   done
 
-nominal_primrec
+nominal_function
     subst  :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
 where
   "subst s t (Var x) = (if (s = x) then t else (Var x))"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/LetFun.thy
--- a/Nominal/Ex/LetFun.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetFun.thy	Mon May 19 12:45:26 2014 +0100
@@ -40,4 +40,4 @@
 thm exp_pat.supp
 
 
-end
\ No newline at end of file
+end
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/LetInv.thy
--- a/Nominal/Ex/LetInv.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetInv.thy	Mon May 19 12:45:26 2014 +0100
@@ -223,7 +223,7 @@
   apply (simp add: Abs_eq_iff alphas supp_atom fresh_star_def neq)
   done
 
-nominal_primrec
+nominal_function
     subst  :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
 where
   "subst s t (Var x) = (if (s = x) then t else (Var x))"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/LetRec.thy
--- a/Nominal/Ex/LetRec.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetRec.thy	Mon May 19 12:45:26 2014 +0100
@@ -28,7 +28,7 @@
 thm let_rec.size_eqvt
 
 
-nominal_primrec
+nominal_function
     height_trm :: "trm \<Rightarrow> nat"
 and height_bp :: "bp \<Rightarrow> nat"
 where
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/LetRecFunNo.thy
--- a/Nominal/Ex/LetRecFunNo.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetRecFunNo.thy	Mon May 19 12:45:26 2014 +0100
@@ -17,7 +17,7 @@
   "bn ANil = []"
 | "bn (ACons x t as) = (atom x) # (bn as)"
 
-nominal_primrec substrec where
+nominal_function substrec where
   "substrec fa fl fd y z (Var x) = (if (y = x) then z else (Var x))"
 | "substrec fa fl fd y z (App l r) = fa l r"
 | "(set (bn as) \<sharp>* (Let as t, y, z) \<and> (\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let as t = Let bs s \<longrightarrow> fl as t = fl bs s)) \<Longrightarrow>
@@ -55,7 +55,7 @@
   done
 termination (eqvt) by lexicographic_order
 
-nominal_primrec substarec :: "(name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn) \<Rightarrow> assn \<Rightarrow> assn" where
+nominal_function substarec :: "(name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn) \<Rightarrow> assn \<Rightarrow> assn" where
   "substarec fac ANil = ANil"
 | "substarec fac (ACons x t as) = fac x t as"
   unfolding eqvt_def substarec_graph_def
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/LetSimple1.thy
--- a/Nominal/Ex/LetSimple1.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetSimple1.thy	Mon May 19 12:45:26 2014 +0100
@@ -25,7 +25,7 @@
 thm trm.strong_exhaust
 thm trm.perm_bn_simps
 
-nominal_primrec
+nominal_function
     height_trm :: "trm \<Rightarrow> nat"
 where
   "height_trm (Var x) = 1"
@@ -51,7 +51,7 @@
   by lexicographic_order
 
 
-nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
+nominal_function (invariant "\<lambda>x (y::atom set). finite y")
   frees_set :: "trm \<Rightarrow> atom set"
 where
   "frees_set (Var x) = {atom x}"
@@ -79,7 +79,7 @@
   by lexicographic_order
 
 
-nominal_primrec
+nominal_function
   subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm"  ("_ [_ ::= _]" [90, 90, 90] 90)
 where
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
@@ -108,4 +108,4 @@
   by lexicographic_order
 
 
-end
\ No newline at end of file
+end
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/LetSimple2.thy
--- a/Nominal/Ex/LetSimple2.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetSimple2.thy	Mon May 19 12:45:26 2014 +0100
@@ -111,7 +111,7 @@
 done
 
 
-nominal_primrec
+nominal_function
     height_trm :: "trm \<Rightarrow> nat"
 where
   "height_trm (Var x) = 1"
@@ -143,7 +143,7 @@
 termination by lexicographic_order
 *)
 
-nominal_primrec 
+nominal_function 
   subst_trm :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm"  ("_ [_ ::= _]" [90, 90, 90] 90) 
 where
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
@@ -197,7 +197,7 @@
 
 
 
-nominal_primrec 
+nominal_function 
 <<<<<<< variant A
  (invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> alpha_bn_preserve (height_assn2::assn \<Rightarrow> nat) x2")
 >>>>>>> variant B
@@ -334,7 +334,7 @@
 
 text {* works, but only because no recursion in as *}
 
-nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
+nominal_function (invariant "\<lambda>x (y::atom set). finite y")
   frees_set :: "trm \<Rightarrow> atom set"
 where
   "frees_set (Var x) = {atom x}"
@@ -381,7 +381,7 @@
 done
 
 
-nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
+nominal_function (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
   subst_trm2 :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm"  ("_ [_ ::trm2= _]" [90, 90, 90] 90) and
   subst_assn2 :: "assn \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> assn"  ("_ [_ ::assn2= _]" [90, 90, 90] 90)
 where
@@ -488,4 +488,4 @@
 done
 
 
-end
\ No newline at end of file
+end
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/Let_ExhaustIssue.thy
--- a/Nominal/Ex/Let_ExhaustIssue.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Let_ExhaustIssue.thy	Mon May 19 12:45:26 2014 +0100
@@ -64,7 +64,7 @@
   shows "f as x c = f bs y c"
 sorry
 
-nominal_primrec
+nominal_function
     height_trm :: "trm \<Rightarrow> nat"
 and height_assn :: "assn \<Rightarrow> nat"
 where
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/Local_Contexts.thy
--- a/Nominal/Ex/Local_Contexts.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Local_Contexts.thy	Mon May 19 12:45:26 2014 +0100
@@ -29,7 +29,7 @@
 lemma atom_image_set_eq_supp: "atom ` set xs = supp xs"
 by (metis image_set set_map_atom_eq_supp)
 
-nominal_primrec (in name_subst)
+nominal_function (in name_subst)
   subst :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [120,120,120] 120)
 where
   "(Var x)[xs::=t] = name_subst x xs t"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/NBE.thy
--- a/Nominal/Ex/NBE.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/NBE.thy	Mon May 19 12:45:26 2014 +0100
@@ -88,7 +88,7 @@
 using assms by (auto simp add: fresh_star_def)
   
 
-nominal_primrec  (invariant "\<lambda>x y. case x of Inl (x1, y1) \<Rightarrow> 
+nominal_function  (invariant "\<lambda>x y. case x of Inl (x1, y1) \<Rightarrow> 
   supp y \<subseteq> (supp y1 - set (bn x1)) \<union> (fv_bn x1) | Inr (x2, y2) \<Rightarrow> supp y \<subseteq> supp x2 \<union> supp y2")
   evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
   evals_aux :: "sem \<Rightarrow> sem \<Rightarrow> sem"
@@ -346,7 +346,7 @@
 done
 
 
-nominal_primrec
+nominal_function
   reify :: "sem \<Rightarrow> lam" and
   reifyn :: "neu \<Rightarrow> lam"
 where
@@ -543,4 +543,4 @@
 where
   "normalize t = reify (eval t)"
 
-end
\ No newline at end of file
+end
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/PaperTest.thy
--- a/Nominal/Ex/PaperTest.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/PaperTest.thy	Mon May 19 12:45:26 2014 +0100
@@ -300,4 +300,4 @@
 apply(relation "measure (\<lambda>(_, t). size t)")
 apply(simp_all)
 
-end
\ No newline at end of file
+end
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/Pi.thy
--- a/Nominal/Ex/Pi.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/Pi.thy	Mon May 19 12:45:26 2014 +0100
@@ -27,7 +27,7 @@
     by(auto)
 qed
 
-nominal_primrec
+nominal_function
   subst_name_list :: "name \<Rightarrow> (name \<times> name) list \<Rightarrow> name"
 where
   "subst_name_list a [] = a"
@@ -143,7 +143,7 @@
   shows "(p \<bullet> (Sum_Type.projl (Sum_Type.projr f))) = Sum_Type.projl (Sum_Type.projr (p \<bullet> f))"
 using a by auto
 
-nominal_primrec (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
+nominal_function (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
   subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix"  ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and
   subsList_mix  :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix"          ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and
   subs_mix      :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix"                      ("_[_::=\<onesuperior>_]" [100, 100, 100] 100)
@@ -568,4 +568,4 @@
 nominal_inductive fresh_list_mix
   done
 
-end
\ No newline at end of file
+end
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))"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/SFT/LambdaTerms.thy
--- a/Nominal/Ex/SFT/LambdaTerms.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/SFT/LambdaTerms.thy	Mon May 19 12:45:26 2014 +0100
@@ -16,7 +16,7 @@
   App (infixl "\<cdot>" 98) and
   Lam ("\<integral> _. _" [97, 97] 99)
 
-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))"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/SubstNoFcb.thy
--- a/Nominal/Ex/SubstNoFcb.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/SubstNoFcb.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 lam_rec ::
+nominal_function lam_rec ::
   "(name \<Rightarrow> 'a :: pt) \<Rightarrow> (lam \<Rightarrow> lam \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> lam \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b :: fs \<Rightarrow> lam \<Rightarrow> 'a"
 where
   "lam_rec fv fa fl fd P (Var n) = fv n"
@@ -49,7 +49,7 @@
   using Abs1_eq_iff lam.eq_iff apply metis
   done
 
-nominal_primrec substr where
+nominal_function substr where
 [simp del]: "substr l y s = lam_rec
   (%x. if x = y then s else (Var x))
   (%t1 t2. App (substr t1 y s) (substr t2 y s))
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|}"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/TypeSchemes2.thy
--- a/Nominal/Ex/TypeSchemes2.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/TypeSchemes2.thy	Mon May 19 12:45:26 2014 +0100
@@ -61,7 +61,7 @@
 using a
 by clarsimp
 
-nominal_primrec (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
+nominal_function (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
     subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
 where
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Nominal2.thy	Mon May 19 12:45:26 2014 +0100
@@ -3,7 +3,7 @@
   Nominal2_Base Nominal2_Abs Nominal2_FCB
 keywords
   "nominal_datatype" :: thy_decl and
-  "nominal_primrec" "nominal_inductive" :: thy_goal and
+  "nominal_function" "nominal_inductive" :: thy_goal and
   "avoids" "binds"
 begin
 
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/nominal_function.ML	Mon May 19 12:45:26 2014 +0100
@@ -275,7 +275,7 @@
 
 (* nominal *)
 val _ =
-  Outer_Syntax.local_theory_to_proof' @{command_spec "nominal_primrec"}
+  Outer_Syntax.local_theory_to_proof' @{command_spec "nominal_function"}
     "define general recursive nominal functions"
        (nominal_function_parser nominal_default_config
           >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))
diff -r 08c3ef07cef7 -r 5ebd327ffb96 README
--- a/README	Mon May 19 11:19:48 2014 +0100
+++ b/README	Mon May 19 12:45:26 2014 +0100
@@ -6,6 +6,12 @@
 
 isabelle build -d . -g Tests
 
+The version of Nominal2 in the AFP can be tested with
+
+isabelle build -d . Nominal2
+isabelle build -d . Launchbury 
+
+
 
 Subdirectories:
 ===============
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Tutorial/Lambda.thy
--- a/Tutorial/Lambda.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Tutorial/Lambda.thy	Mon May 19 12:45:26 2014 +0100
@@ -32,7 +32,7 @@
 
 subsection {* Height Function *}
 
-nominal_primrec
+nominal_function
   height :: "lam \<Rightarrow> int"
 where
   "height (Var x) = 1"
@@ -53,7 +53,7 @@
 
 subsection {* Capture-Avoiding Substitution *}
 
-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))"
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Tutorial/Minimal.thy
--- a/Tutorial/Minimal.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Tutorial/Minimal.thy	Mon May 19 12:45:26 2014 +0100
@@ -15,4 +15,4 @@
   shows "Lam [x]. (Var x) = Lam [y]. (Var y)"
   by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)
 
-end
\ No newline at end of file
+end
diff -r 08c3ef07cef7 -r 5ebd327ffb96 Tutorial/Tutorial6.thy
--- a/Tutorial/Tutorial6.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Tutorial/Tutorial6.thy	Mon May 19 12:45:26 2014 +0100
@@ -46,4 +46,4 @@
   by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def)
 
 
-end
\ No newline at end of file
+end