Now the classical sets include UN_E, to avoid calling hyp_subst_tac

--- a/src/ZF/ZF.ML	Thu Apr 06 12:11:05 1995 +0200
+++ b/src/ZF/ZF.ML	Thu Apr 06 12:15:27 1995 +0200
@@ -411,11 +411,14 @@
     swap_res_tac [minor] 1,
     assume_tac 1 ]);
 
-(*A claset that leaves <= formulae unchanged!*)
+(*A claset that leaves <= formulae unchanged!
+  UN_E appears before UnionE so that it is tried first, to avoid expensive
+  calls to hyp_subst_tac.  Cannot include UN_I as it is unsafe: 
+  would enlarge the search space.*)
 val subset0_cs = FOL_cs
   addSIs [ballI, InterI, CollectI, PowI, empty_subsetI]
   addIs [bexI, UnionI, ReplaceI, RepFunI]
-  addSEs [bexE, make_elim PowD, UnionE, ReplaceE2, RepFunE,
+  addSEs [bexE, make_elim PowD, UN_E, UnionE, ReplaceE2, RepFunE,
 	  CollectE, emptyE]
   addEs [rev_ballE, InterD, make_elim InterD, subsetD];