--- a/Nominal/Ex/Lambda.thy	Mon Jul 18 00:21:51 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Mon Jul 18 10:50:21 2011 +0100
@@ -221,8 +221,7 @@
 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt)
 done
 
-termination
-  by lexicographic_order
+termination by lexicographic_order
 
 text {* a small test lemma *}
 lemma shows "supp t = set (frees_lst t)"
@@ -480,7 +479,6 @@
   apply (auto simp add: fresh_star_def)[3]
   apply(simp_all)
   apply(erule conjE)+
-  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)
@@ -555,14 +553,6 @@
 | DBApp db db
 | DBLam db
 
-lemma option_map_eqvt[eqvt]:
-  "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)"
-  by (cases x) (simp_all, simp add: permute_fun_app_eq)
-
-lemma option_bind_eqvt[eqvt]:
-  shows "(p \<bullet> (Option.map f c)) = (Option.map (p \<bullet> f) (p \<bullet> c))"
-  by (cases c) (simp_all, simp add: permute_fun_app_eq)
-
 instance db :: pure
   apply default
   apply (induct_tac x rule: db.induct)
@@ -583,8 +573,6 @@
   "(p \<bullet> vindex l v n) = vindex (p \<bullet> l) (p \<bullet> v) (p \<bullet> n)"
   by (induct l arbitrary: n) (simp_all add: permute_pure)
 
-
-
 nominal_primrec
   transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option"
 where
@@ -628,8 +616,8 @@
   using a by simp
 
 lemma supp_subst:
-  "supp (t[x ::= s]) \<subseteq> supp t \<union> supp s"
-  by (induct t x s rule: subst.induct) (auto simp add: lam.supp)
+  shows "supp (t[x ::= s]) \<subseteq> (supp t - {atom x}) \<union> supp s"
+  by (induct t x s rule: subst.induct) (auto simp add: lam.supp supp_at_base)
 
 lemma var_fresh_subst:
   "atom x \<sharp> s \<Longrightarrow> atom x \<sharp> (t[x ::= s])"

--- a/Nominal/Nominal2_Base.thy	Mon Jul 18 00:21:51 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Mon Jul 18 10:50:21 2011 +0100
@@ -1088,6 +1088,13 @@
 by (induct xs) (simp_all add: permute_pure)
 
 
+subsubsection {* Equivariance for @{typ "'a option"} *}
+
+lemma option_map_eqvt[eqvt]:
+  shows "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)"
+  by (cases x) (simp_all, simp add: permute_fun_app_eq)
+
+
 subsubsection {* Equivariance for @{typ "'a fset"} *}
 
 lemma in_fset_eqvt [eqvt]: