diff --git a/src/frontends/lean/module_parser.cpp b/src/frontends/lean/module_parser.cpp
index 428db1300f..64adc1c178 100644
--- a/src/frontends/lean/module_parser.cpp
+++ b/src/frontends/lean/module_parser.cpp
@@ -34,7 +34,7 @@ module_parser::~module_parser() {}
 
 pair<cancellation_token, task<module_parser_result>>
 module_parser::resume(module_parser_result const & res, optional<std::vector<gtask>> const & dependencies) {
-    auto & s = *res.m_snapshot_at_end;
+    snapshot const & s = *res.m_snapshot_at_end;
     m_parser.m_scanner.skip_to_pos(s.m_pos);
     m_parser.m_env = s.m_env;
     m_parser.m_ios.set_options(s.m_options);
@@ -47,7 +47,7 @@ module_parser::resume(module_parser_result const & res, optional<std::vector<gta
     m_parser.m_ignore_noncomputable = s.m_noncomputable_theory;
     m_parser.m_parser_scope_stack = s.m_parser_scope_stack;
     m_parser.m_next_inst_idx      = s.m_next_inst_idx;
-
+    set_fresh_name_generator(s.m_name_gen_snapshot);
     auto lt = res.m_lt;
     scope_log_tree_core scope_lt(&lt);
     return parse_next_command_like(dependencies);
diff --git a/src/frontends/lean/module_parser.h b/src/frontends/lean/module_parser.h
index 5c06fa58d7..9acd995b0f 100644
--- a/src/frontends/lean/module_parser.h
+++ b/src/frontends/lean/module_parser.h
@@ -43,7 +43,7 @@ class module_parser : public std::enable_shared_from_this<module_parser> {
 
 public:
     module_parser(std::string const & file_name, std::string const & content,
-                     environment const & initial_env, module_loader const & import_fn);
+                  environment const & initial_env, module_loader const & import_fn);
     ~module_parser();
 
     void use_separate_tasks(bool separate_tasks) { m_separate_tasks = separate_tasks; }
diff --git a/src/frontends/lean/parser_state.h b/src/frontends/lean/parser_state.h
index 5b5fddee9e..bddb0d53ee 100644
--- a/src/frontends/lean/parser_state.h
+++ b/src/frontends/lean/parser_state.h
@@ -522,12 +522,15 @@ struct snapshot {
     parser_scope_stack m_parser_scope_stack;
     unsigned           m_next_inst_idx;
     pos_info           m_pos;
+    name_generator     m_name_gen_snapshot;
     snapshot(environment const & env, local_level_decls const & lds,
              local_expr_decls const & eds, name_set const & lvars, name_set const & vars,
              name_set const & includes, options const & opts, bool imports_parsed, bool noncomputable_theory, parser_scope_stack const & pss,
              unsigned next_inst_idx, pos_info const & pos):
         m_env(env), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes),
-        m_options(opts), m_imports_parsed(imports_parsed), m_noncomputable_theory(noncomputable_theory), m_parser_scope_stack(pss), m_next_inst_idx(next_inst_idx), m_pos(pos) {}
+        m_options(opts), m_imports_parsed(imports_parsed), m_noncomputable_theory(noncomputable_theory),
+        m_parser_scope_stack(pss), m_next_inst_idx(next_inst_idx), m_pos(pos),
+        m_name_gen_snapshot(get_fresh_name_generator_snapshot()) {}
 };
 
 }