--- a/src/HOL/Option.thy Mon Aug 07 11:21:07 2017 +0200
+++ b/src/HOL/Option.thy Mon Aug 07 11:21:11 2017 +0200
@@ -5,7 +5,7 @@
section \<open>Datatype option\<close>
theory Option
-imports Lifting Finite_Set
+ imports Lifting
begin
datatype 'a option =