--- a/Nominal/Abs.thy	Tue Mar 23 07:39:10 2010 +0100
+++ b/Nominal/Abs.thy	Tue Mar 23 07:43:20 2010 +0100
@@ -673,25 +673,5 @@
   apply(simp)
   done
 
-lemma alpha_gen_compose_eqvt:
-  fixes  pia
-  assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
-  and     c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)"
-  and     a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
-  shows  "(g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f (pi \<bullet> pia) (g (pi \<bullet> e), pi \<bullet> s)"
-  using b
-  apply -
-  apply(simp add: alpha_gen.simps)
-  apply(erule conjE)+
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
-  apply(subst permute_eqvt[symmetric])
-  apply(simp)
-  sorry
-
 end
 

--- a/Nominal/Test.thy	Tue Mar 23 07:39:10 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 23 07:43:20 2010 +0100
@@ -2,8 +2,6 @@
 imports "Parser" "../Attic/Prove"
 begin
 
-text {* example 1, equivalent to example 2 from Terms *}
-
 atom_decl name
 
 ML {* val _ = recursive := false *}
@@ -89,6 +87,8 @@
   then show "P c lm" by simp
 qed
 
+text {* example 1, equivalent to example 2 from Terms *}
+
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"