--- a/Nominal/Abs.thy	Wed Apr 14 20:21:11 2010 +0200
+++ b/Nominal/Abs.thy	Wed Apr 14 22:23:52 2010 +0200
@@ -762,7 +762,7 @@
   by (simp_all add: fresh_plus_perm)
 
 
-lemma alpha_gen_eqvt[eqvt]:
+lemma alpha_gen_eqvt(*[eqvt]*):
   shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
   and   "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
   and   "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" 

--- a/Nominal/Ex/Lambda.thy	Wed Apr 14 20:21:11 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Wed Apr 14 22:23:52 2010 +0200
@@ -9,6 +9,8 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l
 
+thm lam.fv
+thm lam.supp
 lemmas supp_fn' = lam.fv[simplified lam.supp]
 
 declare lam.perm[eqvt]
@@ -151,24 +153,17 @@
   | t'_App[intro]: "\<lbrakk>\<Gamma> |\<Turnstile> t1 : T1\<rightarrow>T2; \<Gamma> |\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> App t1 t2 : T2"
   | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> |\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Lam x t : T1\<rightarrow>T2"
 
-use "../../Nominal-General/nominal_eqvt.ML"
-
 equivariance valid
 equivariance typing
+equivariance typing'
+equivariance typing2' 
+equivariance typing''
 
 thm valid.eqvt
 thm typing.eqvt
 thm eqvts
 thm eqvts_raw
 
-equivariance typing'
-equivariance typing2' 
-equivariance typing''
-
-ML {*
-fun mk_minus p = 
- Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p
-*}
 
 inductive
   tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"