# HG changeset patch
# User paulson
# Date 835953372 -7200
# Node ID ce5dc74dec972701b05afb89c8616cf958a9a8a0
# Parent  861e29c7cadacb65aae76c4da31a521e241f38e7
Now set_cs is just taken from !claset

diff -r 861e29c7cada -r ce5dc74dec97 src/HOL/Fun.ML
--- 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");