--- a/src/HOL/Finite_Set.thy Fri Aug 13 10:38:28 2010 +0200
+++ b/src/HOL/Finite_Set.thy Fri Aug 13 10:51:23 2010 +0200
@@ -6,7 +6,7 @@
header {* Finite sets *}
theory Finite_Set
-imports Power Option
+imports Option Power
begin
subsection {* Predicate for finite sets *}