src/HOL/Sum.ML

 goalw Sum.thy [Part_def] "!!a. a : Part A h ==> a : A";
 by (etac IntD1 1);
 qed "PartD1";
 
 goal Sum.thy "Part A (%x.x) = A";
-by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
 qed "Part_id";
 
 goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
-by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
 qed "Part_Int";
 
 (*For inductive definitions*)
 goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
-by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
 qed "Part_Collect";