# HG changeset patch
# User paulson
# Date 1031756039 -7200
# Node ID 40e4755e57f7c54b673eea6cf5f7c6ed01699c41
# Parent  1500a2e48d443d3c27e6e386a0ab01f913df3228
Bound variable preservation in Collect_cong

diff -r 1500a2e48d44 -r 40e4755e57f7 src/ZF/ZF.ML
--- 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";