--- a/Nominal/Ex/Lambda.thy	Wed Jun 01 21:03:30 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 01 22:55:14 2011 +0100
@@ -10,14 +10,6 @@
 | 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"
@@ -577,7 +569,6 @@
 
 text {* "HO" functions *}
 
-
 nominal_primrec
   trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
 where
@@ -601,8 +592,6 @@
   "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)
-prefer 2
-ML_prf {* prop_of (hd (#prems (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))))) *}
 oops
 
 (* function tests *)