src/CCL/Set.thy

--- a/src/CCL/Set.thy	Wed Jan 12 15:53:37 2011 +0100
+++ b/src/CCL/Set.thy	Wed Jan 12 16:33:04 2011 +0100
@@ -222,7 +222,7 @@
 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