diff -r f2e8984adef7 -r b5d8e57826df 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>