--- a/Nominal/Ex/Lambda.thy	Thu Jul 09 09:12:44 2015 +0100
+++ b/Nominal/Ex/Lambda.thy	Mon Jul 20 11:21:59 2015 +0100
@@ -14,14 +14,6 @@
 
 thm obtain_atom
 
-lemma 
- "(\<forall>thesis. (finite X \<longrightarrow> (\<forall>a. ((a \<notin> X \<and> sort_of a = s) \<longrightarrow> thesis)) \<longrightarrow> thesis)) \<longleftrightarrow>
-  (finite X \<longrightarrow> (\<exists> a. (a \<notin> X \<and> sort_of a = s)))"
-apply(auto) 
-done
-
-
-
 ML {* trace := true *}
 
 nominal_datatype lam =
@@ -996,8 +988,6 @@
 
 text {* tests of functions containing if and case *}
 
-consts P :: "lam \<Rightarrow> bool"
-
 (*
 nominal_function  
   A :: "lam => lam"