diff --git a/library/data/option.lean b/library/data/option.lean
index c2e3c1b324..ad8bcf0eed 100644
--- a/library/data/option.lean
+++ b/library/data/option.lean
@@ -4,10 +4,6 @@
 import logic.eq
 open eq.ops decidable
 
-inductive option (A : Type) : Type :=
-  none {} : option A,
-  some    : A → option A
-
 namespace option
   definition is_none {A : Type} (o : option A) : Prop :=
   rec true (λ a, false) o
diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean
index 8d50342f67..8dda9cca0e 100644
--- a/library/init/datatypes.lean
+++ b/library/init/datatypes.lean
@@ -76,3 +76,7 @@ str   : char → string → string
 inductive nat :=
 zero : nat,
 succ : nat → nat
+
+inductive option (A : Type) : Type :=
+none {} : option A,
+some    : A → option A