src/ZF/ZF.ML

--- a/src/ZF/ZF.ML	Wed Apr 09 12:36:52 1997 +0200
+++ b/src/ZF/ZF.ML	Wed Apr 09 12:37:44 1997 +0200
@@ -438,7 +438,6 @@
  (fn _=> [ Blast_tac 1 ]);
 
 Addsimps [empty_subsetI];
-AddSIs [empty_subsetI];
 
 qed_goal "equals0I" ZF.thy "[| !!y. y:A ==> False |] ==> A=0"
  (fn prems=> [ blast_tac (!claset addDs prems) 1 ]);