diff -r 9ae285ce814e -r 08c3ef07cef7 Nominal/Atoms.thy
--- a/Nominal/Atoms.thy	Fri May 16 08:38:23 2014 +0100
+++ b/Nominal/Atoms.thy	Mon May 19 11:19:48 2014 +0100
@@ -71,34 +71,6 @@
 
 term "a:::name"
 
-text {* 
-  a:::name stands for (atom a) with a being of concrete atom 
-  type name. The above lemma can therefore also be stated as
-
-  "sort_of (a:::name) = Sort ''name'' []"
-
-  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}. *}