diff --git a/src/builtin/basic.olean b/src/builtin/basic.olean
index 4ccb80be95..2c11b4847c 100644
Binary files a/src/builtin/basic.olean and b/src/builtin/basic.olean differ
diff --git a/src/builtin/cast.olean b/src/builtin/cast.olean
index 380e07a788..d706e90323 100644
Binary files a/src/builtin/cast.olean and b/src/builtin/cast.olean differ
diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp
index 1e6c3bf3ca..24cf908b26 100644
--- a/src/frontends/lean/frontend.cpp
+++ b/src/frontends/lean/frontend.cpp
@@ -39,7 +39,7 @@ public:
     virtual char const * keyword() const { return "MarkImplicit"; }
     virtual void write(serializer & s) const {
         unsigned sz = m_implicit.size();
-        s << "MarkImplicit" << m_obj_name << sz;
+        s << "Imp" << m_obj_name << sz;
         for (auto b : m_implicit)
             s << b;
     }
@@ -52,7 +52,7 @@ static void read_mark_implicit(environment const & env, io_state const &, deseri
         implicit.push_back(d.read_bool());
     mark_implicit_arguments(env, n, implicit.size(), implicit.data());
 }
-static object_cell::register_deserializer_fn mark_implicit_ds("MarkImplicit", read_mark_implicit);
+static object_cell::register_deserializer_fn mark_implicit_ds("Imp", read_mark_implicit);
 
 static std::vector<bool> g_empty_vector;
 /**
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index fe346455f9..e7d51f9c8d 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -33,14 +33,14 @@ public:
     set_opaque_command(name const & n, bool opaque):m_obj_name(n), m_opaque(opaque) {}
     virtual ~set_opaque_command() {}
     virtual char const * keyword() const { return "SetOpaque"; }
-    virtual void write(serializer & s) const { s << "SetOpaque" << m_obj_name << m_opaque; }
+    virtual void write(serializer & s) const { s << "Opa" << m_obj_name << m_opaque; }
 };
 static void read_set_opaque(environment const & env, io_state const &, deserializer & d) {
     name n = read_name(d);
     bool o = d.read_bool();
     env->set_opaque(n, o);
 }
-static object_cell::register_deserializer_fn set_opaque_ds("SetOpaque", read_set_opaque);
+static object_cell::register_deserializer_fn set_opaque_ds("Opa", read_set_opaque);
 
 class import_command : public neutral_object_cell {
     std::string m_mod_name;
diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp
index 83ce8a2993..816517439e 100644
--- a/src/kernel/object.cpp
+++ b/src/kernel/object.cpp
@@ -157,14 +157,14 @@ public:
     axiom_object_cell(name const & n, expr const & t):postulate_object_cell(n, t) {}
     virtual char const * keyword() const { return "Axiom"; }
     virtual bool is_axiom() const { return true; }
-    virtual void write(serializer & s) const { s << "Axiom" << get_name() << get_type(); }
+    virtual void write(serializer & s) const { s << "Ax" << get_name() << get_type(); }
 };
 static void read_axiom(environment const & env, io_state const &, deserializer & d) {
     name n    = read_name(d);
     expr t    = read_expr(d);
     env->add_axiom(n, t);
 }
-static object_cell::register_deserializer_fn axiom_ds("Axiom", read_axiom);
+static object_cell::register_deserializer_fn axiom_ds("Ax", read_axiom);
 
 
 /**
@@ -175,14 +175,14 @@ public:
     variable_decl_object_cell(name const & n, expr const & t):postulate_object_cell(n, t) {}
     virtual char const * keyword() const { return "Variable"; }
     virtual bool is_var_decl() const { return true; }
-    virtual void write(serializer & s) const { s << "Variable" << get_name() << get_type(); }
+    virtual void write(serializer & s) const { s << "Var" << get_name() << get_type(); }
 };
 static void read_variable(environment const & env, io_state const &, deserializer & d) {
     name n    = read_name(d);
     expr t    = read_expr(d);
     env->add_var(n, t);
 }
-static object_cell::register_deserializer_fn var_decl_ds("Variable", read_variable);
+static object_cell::register_deserializer_fn var_decl_ds("Var", read_variable);
 
 /**
    \brief Base class for definitions: theorems and definitions.
@@ -202,7 +202,7 @@ public:
     virtual expr get_value() const       { return m_value; }
     virtual char const * keyword() const { return "Definition"; }
     virtual unsigned get_weight() const  { return m_weight; }
-    virtual void write(serializer & s) const { s << "Definition" << get_name() << get_type() << get_value(); }
+    virtual void write(serializer & s) const { s << "Def" << get_name() << get_type() << get_value(); }
 };
 static void read_definition(environment const & env, io_state const &, deserializer & d) {
     name n    = read_name(d);
@@ -210,7 +210,7 @@ static void read_definition(environment const & env, io_state const &, deseriali
     expr v    = read_expr(d);
     env->add_definition(n, t, v);
 }
-static object_cell::register_deserializer_fn definition_ds("Definition", read_definition);
+static object_cell::register_deserializer_fn definition_ds("Def", read_definition);
 
 /**
    \brief Theorems
@@ -223,7 +223,7 @@ public:
     }
     virtual char const * keyword() const { return "Theorem"; }
     virtual bool is_theorem() const { return true; }
-    virtual void write(serializer & s) const { s << "Theorem" << get_name() << get_type() << get_value(); }
+    virtual void write(serializer & s) const { s << "Th" << get_name() << get_type() << get_value(); }
 };
 static void read_theorem(environment const & env, io_state const &, deserializer & d) {
     name n    = read_name(d);
@@ -231,7 +231,7 @@ static void read_theorem(environment const & env, io_state const &, deserializer
     expr v    = read_expr(d);
     env->add_theorem(n, t, v);
 }
-static object_cell::register_deserializer_fn theorem_ds("Theorem", read_theorem);
+static object_cell::register_deserializer_fn theorem_ds("Th", read_theorem);
 
 object mk_uvar_decl(name const & n, level const & l) { return object(new uvar_declaration_object_cell(n, l)); }
 object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight) { return object(new definition_object_cell(n, t, v, weight)); }