--- a/Quot/Nominal/Abs.thy	Mon Feb 08 11:56:22 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Mon Feb 08 13:12:55 2010 +0100
@@ -3,24 +3,11 @@
 begin
 
 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
-lemma in_permute_iff:
-  shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
-apply(unfold mem_def permute_fun_def)[1]
-apply(simp add: permute_bool_def) 
-done
-
-lemma fresh_plus:
-  fixes p q::perm
-  shows "\<lbrakk>a \<sharp> p;  a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)"
-  unfolding fresh_def
-  using supp_plus_perm
-  by(auto)
-
 lemma fresh_star_plus:
   fixes p q::perm
   shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
   unfolding fresh_star_def
-  by (simp add: fresh_plus)
+  by (simp add: fresh_plus_perm)
 
 
 lemma fresh_star_permute_iff:
@@ -34,18 +21,11 @@
 apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])
 apply(simp)
 apply(drule_tac x="- p \<bullet> xa" in bspec)
-apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1])
+apply(rule_tac ?p1="p" in mem_permute_iff[THEN iffD1])
 apply(simp)
 apply(simp)
 done
 
-lemma fresh_minus_perm:
-  fixes p::perm
-  shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
-  apply(simp add: fresh_def)
-  apply(simp only: supp_minus_perm)
-  done
-
 fun
   alpha_gen 
 where