--- a/src/HOL/Fun.ML Fri Jun 28 11:13:07 1996 +0200
+++ b/src/HOL/Fun.ML Fri Jun 28 11:16:12 1996 +0200
@@ -179,14 +179,6 @@
AddEs [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
subsetD, subsetCE];
-val set_cs = HOL_cs
- addSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI,
- ComplI, IntI, DiffI, UnCI, insertCI]
- addIs [bexI, UnionI, UN_I, UN1_I, imageI, rangeI]
- addSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
- make_elim singleton_inject,
- CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE]
- addEs [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
- subsetD, subsetCE];
+val set_cs = !claset delrules [equalityI];
fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac (claset_of "Fun");