expandshort

--- a/src/ZF/equalities.ML	Wed Mar 03 10:32:35 1999 +0100
+++ b/src/ZF/equalities.ML	Wed Mar 03 10:36:24 1999 +0100
@@ -560,7 +560,7 @@
 qed "Pow_0";
 
 Goal "Pow (cons(a,A)) = Pow(A) Un {cons(a,X) . X: Pow(A)}";
-br equalityI 1;
+by (rtac equalityI 1);
 by Safe_tac;
 by (etac swap 1);
 by (res_inst_tac [("a", "x-{a}")] RepFun_eqI 1);