--- a/Nominal/Ex/Lambda.thy	Thu Jun 02 10:09:23 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Thu Jun 02 10:11:50 2011 +0900
@@ -10,6 +10,7 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
+
 inductive 
   triv :: "lam \<Rightarrow> nat \<Rightarrow> bool"
 where
@@ -451,10 +452,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) 
@@ -589,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 *)