--- a/src/ZF/UNITY/WFair.thy Wed Dec 19 11:07:38 2001 +0100
+++ b/src/ZF/UNITY/WFair.thy Wed Dec 19 11:13:27 2001 +0100
@@ -10,7 +10,7 @@
Theory ported from HOL.
*)
-WFair = UNITY +
+WFair = UNITY + Main_ZFC +
constdefs
(* This definition specifies weak fairness. The rest of the theory