src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Tue Mar 01 10:32:55 2016 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Mar 01 10:36:19 2016 +0100
@@ -6,7 +6,7 @@
 section \<open>Finite sets\<close>
 
 theory Finite_Set
-imports Product_Type Sum_Type Nat
+imports Product_Type Sum_Type Fields
 begin
 
 subsection \<open>Predicate for finite sets\<close>