--- a/Nominal/Ex/Lambda.thy	Tue Apr 13 00:53:48 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue Apr 13 07:40:54 2010 +0200
@@ -260,15 +260,6 @@
 using a
 apply(induct)
 apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *})
-apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *})
-apply(perm_strict_simp)
-apply(rule alpha_lam_raw.intros)
-apply(simp)
-apply(perm_strict_simp)
-apply(rule alpha_lam_raw.intros)
-apply(simp add: alphas)
-apply(rule_tac p="- p" in permute_boolE)
-apply(perm_simp permute_minus_cancel(2))
 oops
 
 thm alpha_lam_raw.intros[no_vars]

--- a/Nominal/Nominal2_FSet.thy	Tue Apr 13 00:53:48 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy	Tue Apr 13 07:40:54 2010 +0200
@@ -40,14 +40,15 @@
   by (lifting permute_list.simps)
 
 lemma fmap_eqvt[eqvt]: 
-  shows "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)"
+  shows "p \<bullet> (fmap f l) = fmap (p \<bullet> f) (p \<bullet> l)"
   by (lifting map_eqvt)
 
-lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)"
+lemma fset_to_set_eqvt[eqvt]: 
+  shows "p \<bullet> (fset_to_set x) = fset_to_set (p \<bullet> x)"
   by (lifting set_eqvt)
 
 lemma fin_fset_to_set:
-  "finite (fset_to_set x)"
+  shows "finite (fset_to_set x)"
   by (induct x) (simp_all)
 
 lemma supp_fset_to_set:
@@ -64,9 +65,10 @@
   done
 
 lemma supp_fmap_atom:
-  "supp (fmap atom x) = supp x"
-  apply (simp add: supp_def)
-  apply (simp add: eqvts eqvts_raw atom_fmap_cong)
+  shows "supp (fmap atom x) = supp x"
+  unfolding supp_def
+  apply (perm_simp)
+  apply (simp add: atom_fmap_cong)
   done
 
 lemma supp_atom_insert:
@@ -84,7 +86,9 @@
 lemma atom_eqvt_raw:
   fixes p::"perm"
   shows "(p \<bullet> atom) = atom"
-  by (simp add: expand_fun_eq permute_fun_def atom_eqvt)
+  apply(perm_simp)
+  apply(simp)
+  done
 
 lemma supp_finite_at_set:
   fixes S::"('a :: at) set"