src/ZF/QUniv.ML

--- a/src/ZF/QUniv.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/QUniv.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -193,6 +193,6 @@
 by (rtac (succI1 RS UN_upper) 1);
 (*Limit(i) case*)
 by (asm_simp_tac
-    (simpset() addsimps [Limit_Vfrom_eq, Int_UN_distrib, subset_refl,
+    (simpset() addsimps [Limit_Vfrom_eq, Int_UN_distrib, 
 			 UN_mono, QPair_Int_Vset_subset_trans]) 1);
 qed "QPair_Int_Vset_subset_UN";