tidied some awkward proofs

--- a/src/HOL/equalities.ML	Tue Oct 17 10:26:07 2000 +0200
+++ b/src/HOL/equalities.ML	Tue Oct 17 10:27:28 2000 +0200
@@ -843,17 +843,11 @@
 Addsimps [Pow_empty];
 
 Goal "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
-by Safe_tac;
-by (etac swap 1);
-by (res_inst_tac [("x", "x-{a}")] image_eqI 1);
-by (ALLGOALS Blast_tac);
+by (blast_tac (claset() addIs [inst "x" "?u-{a}" image_eqI]) 1);
 qed "Pow_insert";
 
 Goal "Pow (- A) = {-B |B. A: Pow B}";
-by Safe_tac;
-by (Blast_tac 2);
-by (res_inst_tac [("x", "-x")] exI 1);
-by (ALLGOALS Blast_tac);
+by (blast_tac (claset() addIs [inst "x" "- ?u" exI]) 1);
 qed "Pow_Compl";
 
 Goal "Pow UNIV = UNIV";