src/ZF/UNITY/Union.thy

--- a/src/ZF/UNITY/Union.thy	Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/UNITY/Union.thy	Sun Nov 20 20:15:02 2011 +0100
@@ -427,7 +427,7 @@
 lemma ok_commute: "(F ok G) <->(G ok F)"
 by (auto simp add: ok_def)
 
-lemmas ok_sym = ok_commute [THEN iffD1, standard]
+lemmas ok_sym = ok_commute [THEN iffD1]
 
 lemma ok_iff_OK: "OK({<0,F>,<1,G>,<2,H>}, snd) <-> (F ok G & (F Join G) ok H)"
 by (simp add: ok_def Join_def OK_def Int_assoc cons_absorb