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