src/ZF/Finite.thy

--- a/src/ZF/Finite.thy	Mon Feb 11 15:19:17 2008 +0100
+++ b/src/ZF/Finite.thy	Mon Feb 11 15:40:21 2008 +0100
@@ -8,7 +8,7 @@
 
 header{*Finite Powerset Operator and Finite Function Space*}
 
-theory Finite imports Inductive Epsilon Nat begin
+theory Finite imports Inductive_ZF Epsilon Nat_ZF begin
 
 (*The natural numbers as a datatype*)
 rep_datatype