src/ZF/equalities.ML

--- a/src/ZF/equalities.ML	Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/equalities.ML	Thu Jan 07 10:56:05 1999 +0100
@@ -602,7 +602,8 @@
 by (Blast_tac 1);
 qed "Collect_Diff";
 
-Goal "{x:cons(a,B). P(x)} = if(P(a), cons(a, {x:B. P(x)}), {x:B. P(x)})";
+Goal "{x:cons(a,B). P(x)} = \
+\     (if P(a) then cons(a, {x:B. P(x)}) else {x:B. P(x)})";
 by (simp_tac (simpset() addsplits [split_if]) 1);
 by (Blast_tac 1);
 qed "Collect_cons";