--- a/Nominal/Ex/Lambda.thy	Wed Jun 01 16:13:42 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 01 21:03:30 2011 +0100
@@ -10,6 +10,15 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
+nominal_primrec
+  Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
+where
+  "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
+unfolding eqvt_def Z_graph_def
+apply (rule, perm_simp, rule)
+oops
+
+
 inductive 
   triv :: "lam \<Rightarrow> nat \<Rightarrow> bool"
 where
@@ -451,10 +460,12 @@
   apply auto
   done
 
+(*
 lemma db_trans_test:
   assumes a: "y \<noteq> x"
   shows "trans (Lam [x]. Lam [y]. App (Var x) (Var y)) [] 0 = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))"
   using a by simp
+*)
 
 abbreviation
   mbind :: "'a option => ('a => 'b option) => 'b option"  ("_ \<guillemotright>= _" [65,65] 65) 
@@ -566,6 +577,7 @@
 
 text {* "HO" functions *}
 
+
 nominal_primrec
   trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
 where