src/ZF/equalities.thy

--- a/src/ZF/equalities.thy	Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/equalities.thy	Sun Nov 20 20:15:02 2011 +0100
@@ -81,7 +81,7 @@
 
 (*A safe special case of subset elimination, adding no new variables 
   [| cons(a,B) \<subseteq> C; [| a \<in> C; B \<subseteq> C |] ==> R |] ==> R *)
-lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE, standard]
+lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE]
 
 lemma subset_empty_iff: "A\<subseteq>0 <-> A=0"
 by blast