--- a/Nominal/Abs.thy	Tue Mar 02 15:05:35 2010 +0100
+++ b/Nominal/Abs.thy	Tue Mar 02 15:05:50 2010 +0100
@@ -351,8 +351,6 @@
 notation 
   alpha1 ("_ \<approx>abs1 _")
 
-thm swap_set_not_in
-
 lemma qq:
   fixes S::"atom set"
   assumes a: "supp p \<inter> S = {}"
@@ -502,6 +500,15 @@
 apply(simp)
 oops
 
+fun
+  distinct_perms 
+where
+  "distinct_perms [] = True"
+| "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)"
+
+
+
+
 
 end