--- a/Nominal/Atoms.thy	Mon Mar 14 16:35:59 2011 +0100
+++ b/Nominal/Atoms.thy	Tue Mar 15 00:40:39 2011 +0100
@@ -80,6 +80,25 @@
   This does not work for multi-sorted atoms.
 *}
 
+(* fixme 
+lemma supp_of_finite_name_set:
+  fixes S::"name set"
+  assumes "infinte S" "infinite (UNIV - S)"
+  shows "supp S = UNIV"
+proof -
+  { fix a    
+    have "a \<in> supp S"
+    proof (cases "a \<in> atom ` S")
+      assume "a \<in> atom ` S"
+      then have "\<forall>b \<in> UNIV - S. (a \<rightleftharpoons> atom b) \<bullet> S \<noteq> S"
+	apply(clarify)
+	
+      show "a \<in> supp S"
+  }
+  then show "supp S = UNIV" by auto
+qed
+*)
+
 
 section {* Automatic instantiation of class @{text at}. *}