diff --git a/src/library/choice.cpp b/src/library/choice.cpp
index 7c15af4533..c6cb7ff49a 100644
--- a/src/library/choice.cpp
+++ b/src/library/choice.cpp
@@ -7,10 +7,13 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "library/choice.h"
 #include "library/kernel_bindings.h"
+#include "library/kernel_serializer.h"
 
 namespace lean {
 static name g_choice_name("choice");
-[[ noreturn ]] static void throw_ex() { throw exception("unexpected occurrence of 'choice' expression"); }
+static std::string g_choice_opcode("Choice");
+[[ noreturn ]] static void throw_ex() { throw exception("unexpected occurrence of 'choice' expression");
+}
 
 // We encode a 'choice' expression using a macro.
 // This is a trick to avoid creating a new kind of expression.
@@ -23,7 +26,10 @@ public:
     // Choice expressions cannot be exported. They are transient/auxiliary objects.
     virtual expr get_type(expr const &, expr const *, extension_context &) const { throw_ex(); }
     virtual optional<expr> expand(expr const &, extension_context &) const { throw_ex(); }
-    virtual void write(serializer &) const { throw_ex(); }
+    virtual void write(serializer & s) const {
+        // we should be able to write choice expressions because of notation declarations
+        s.write_string(g_choice_opcode);
+    }
 };
 
 static macro_definition g_choice(new choice_macro_cell());
@@ -35,6 +41,9 @@ expr mk_choice(unsigned num_es, expr const * es) {
         return mk_macro(g_choice, num_es, es);
 }
 
+static register_macro_deserializer_fn
+choice_macro_des_fn(g_choice_opcode, [](deserializer &, unsigned num, expr const * args) { return mk_choice(num, args); });
+
 bool is_choice(expr const & e) {
     return is_macro(e) && macro_def(e) == g_choice;
 }