--- a/src/ZF/Epsilon.thy Mon Feb 11 15:19:17 2008 +0100
+++ b/src/ZF/Epsilon.thy Mon Feb 11 15:40:21 2008 +0100
@@ -7,7 +7,7 @@
header{*Epsilon Induction and Recursion*}
-theory Epsilon imports Nat begin
+theory Epsilon imports Nat_ZF begin
definition
eclose :: "i=>i" where