diff -r 8aca34dbe195 -r fa3247e6ee4b src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Mon Aug 07 11:21:07 2017 +0200
+++ b/src/HOL/Lattices_Big.thy	Mon Aug 07 11:21:11 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\<close>
 
 theory Lattices_Big
-imports Finite_Set Option
+  imports Option
 begin
 
 subsection \<open>Generic lattice operations over a set\<close>