--- a/Nominal/Abs.thy	Tue Mar 02 15:07:27 2010 +0100
+++ b/Nominal/Abs.thy	Tue Mar 02 16:03:19 2010 +0100
@@ -500,5 +500,14 @@
 oops
 
 *)
+
+fun
+  distinct_perms 
+where
+  "distinct_perms [] = True"
+| "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)"
+
+
+
 end