src/CCL/Set.thy

   assumes "~ A={}"
   shows "EX x. x:A"
 proof -
   have "\<not> (EX x. x:A) \<Longrightarrow> A = {}"
     by (rule equalityI) (blast intro!: subsetI elim!: emptyD)+
-  with prems show ?thesis by blast
+  with assms show ?thesis by blast
 qed
 
 
 subsection {* Singleton sets *}