--- a/src/HOL/Prod.ML Wed Mar 01 12:26:28 2000 +0100
+++ b/src/HOL/Prod.ML Wed Mar 01 15:00:21 2000 +0100
@@ -142,7 +142,7 @@
qed "split_weak_cong";
Goal "(%u. ? x y. u = (x, y) & P (x, y)) = P";
-br ext 1;
+by (rtac ext 1);
by (Fast_tac 1);
qed "split_eta_SetCompr";
Addsimps [split_eta_SetCompr];