--- a/Nominal/Ex/Lambda.thy	Fri Apr 16 11:09:32 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Fri Apr 16 16:29:11 2010 +0200
@@ -188,56 +188,28 @@
 
 declare permute_lam_raw.simps[eqvt]
 declare alpha_gen_eqvt[eqvt]
-(*equivariance alpha_lam_raw'*)
+equivariance alpha_lam_raw'
 thm eqvts_raw
 
+
+
+(* HERE *)
+
 lemma
   assumes a: "alpha_lam_raw' t1 t2"
   shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)"
 using a
 apply(induct)
-apply(perm_simp)
-apply(rule a1)
-apply(simp)
-apply(perm_simp)
-apply(rule a2)
-apply(simp)
-apply(simp)
-
-apply simp
-apply (rule a3)
-apply (erule exi[of _ _ "p"])
-apply (simp add: alphas)
-apply (erule conjE)+
-apply (rule conjI)
-apply (rule permute_eq_iff[of "- p", THEN iffD1])
-apply (simp add: eqvts)
-apply (rule conjI)
-apply (rule fresh_star_permute_iff[of "- p", THEN iffD1])
-apply (simp add: eqvts)
-apply (rule conjI)
-apply (simp add: permute_eqvt[symmetric])
-apply (rule permute_eq_iff[of "- p", THEN iffD1])
-apply (subst permute_eqvt)
-apply (simp add: eqvts)
-done
-
-lemma
-  assumes a: "alpha_lam_raw' t1 t2"
-  shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)"
-using a
-apply(induct)
-ML_prf {*
-val ({names, ...}, {raw_induct, intrs, ...}) =
-    Inductive.the_inductive @{context} (Sign.intern_const @{theory} "alpha_lam_raw")
-*}
+apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
+  @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a1} 1*})
 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
-  @{context} ["Lambda.alpha_lam_raw"] @{term "p::perm"} @{thm a1} 1*})
+  @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a2} 1*})
+(*
 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
-  @{context} ["Lambda.alpha_lam_raw"] @{term "p::perm"} @{thm a2} 1*})
+  @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a3} 1*})
+*)
 oops
 
-
 section {* size function *}
 
 lemma size_eqvt_raw: