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)"