--- a/Nominal/Ex/Lambda.thy	Tue Jul 05 15:01:10 2011 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue Jul 05 16:22:18 2011 +0200
@@ -19,7 +19,7 @@
  let
    val _ = Inductive.the_inductive ctxt "local.frees_lst_graph"
  in 
-   Method.SIMPLE_METHOD' (K all_tac)
+   Method.SIMPLE_METHOD' (K (all_tac))
  end)
 *}
 
@@ -85,14 +85,6 @@
 lemma "frees_set t = supp t"
   by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base)
 
-lemma fresh_fun_eqvt_app3:
-  assumes a: "eqvt f"
-  and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z"
-  shows "a \<sharp> f x y z"
-  using fresh_fun_eqvt_app[OF a b(1)] a b
-  by (metis fresh_fun_app)
-
-
 section {* height function *}
 
 nominal_primrec
@@ -317,7 +309,8 @@
   apply (auto simp add: fresh_star_def)[3]
   apply(simp_all)
   apply(erule conjE)+
-  apply (erule_tac Abs_lst1_fcb2')
+  thm Abs_lst1_fcb2'
+  apply (erule_tac c="xsa" in Abs_lst1_fcb2')
   apply (simp add: fresh_star_def)
   apply (simp add: fresh_star_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
@@ -664,9 +657,7 @@
   apply(auto)[1]
   apply(simp_all)[44]
   apply(simp del: Product_Type.prod.inject)  
-  sorry
-
-termination by lexicographic_order
+  oops
 
 lemma abs_same_binder:
   fixes t ta s sa :: "_ :: fs"