# HG changeset patch
# User paulson
# Date 920453784 -3600
# Node ID a336f80158c8c16b0abb40eae039eceb2b481625
# Parent  5b9fbdfe22b7a1d9e42b392c8ea422a8b9709c5a
expandshort

diff -r 5b9fbdfe22b7 -r a336f80158c8 src/ZF/equalities.ML
--- 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);