Bound variable preservation in Collect_cong

--- a/src/ZF/ZF.ML	Tue Sep 10 16:51:31 2002 +0200
+++ b/src/ZF/ZF.ML	Wed Sep 11 16:53:59 2002 +0200
@@ -321,7 +321,8 @@
 qed "CollectD2";
 
 val prems= Goalw [Collect_def]  
-    "[| A=B;  !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)";
+    "[| A=B;  !!x. x:B ==> P(x) <-> Q(x) |] \
+\    ==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))";
 by (simp_tac (simpset() addsimps prems) 1) ;
 qed "Collect_cong";