diff -r b8d0d8407c3b -r e8c5e95d338b src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Big_Operators.thy	Thu Nov 21 21:33:34 2013 +0100
@@ -6,7 +6,7 @@
 header {* Big operators and finite (non-empty) sets *}
 
 theory Big_Operators
-imports Finite_Set Option Metis
+imports Finite_Set Metis
 begin
 
 subsection {* Generic monoid operation over a set *}