diff --git a/src/library/private.cpp b/src/library/private.cpp
index 2493b12ec1..b5f331332d 100644
--- a/src/library/private.cpp
+++ b/src/library/private.cpp
@@ -18,7 +18,8 @@ struct private_ext : public environment_extension {
     /* We store private prefixes to make sure register_private_name is used correctly.
        This information does not need to be stored in .olean files. */
     name_set       m_private_prefixes;
-    private_ext():m_counter(0) {}
+    name           m_mod_name;
+    private_ext():m_counter(1) {}
 };
 
 struct private_ext_reg {
@@ -34,6 +35,12 @@ static environment update(environment const & env, private_ext const & ext) {
     return env.update(g_ext->m_ext_id, std::make_shared<private_ext>(ext));
 }
 
+environment set_main_module_name(environment const & env, name const & mod_name) {
+    private_ext ext = get_extension(env);
+    ext.m_mod_name  = mod_name;
+    return  update(env, ext);
+}
+
 static name * g_private = nullptr;
 
 struct private_modification : public modification {
@@ -48,7 +55,6 @@ struct private_modification : public modification {
         private_ext ext = get_extension(env);
         // we restore only the mapping hidden-name -> user-name (for pretty printing purposes)
         ext.m_inv_map.insert(m_real, m_name);
-        ext.m_counter++;
         env = update(env, ext);
     }
 
@@ -69,16 +75,13 @@ static environment preserve_private_data(environment const & env, name const & r
     return module::add(env, std::make_shared<private_modification>(n, r));
 }
 
-static name mk_private_name_core(environment const & env, name const & n, optional<unsigned> const & extra_hash) {
+static name mk_private_name_core(environment const & env, name const & n) {
     private_ext const & ext = get_extension(env);
-    unsigned h              = hash(n.hash(), ext.m_counter);
-    if (extra_hash)
-        h = hash(h, *extra_hash);
-    return name(*g_private, h) + n;
+    return name(name(*g_private) + ext.m_mod_name, ext.m_counter) + n;
 }
 
-pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & extra_hash) {
-    name r          = mk_private_name_core(env, n, extra_hash);
+pair<environment, name> add_private_name(environment const & env, name const & n) {
+    name r          = mk_private_name_core(env, n);
     private_ext ext = get_extension(env);
     ext.m_inv_map.insert(r, n);
     ext.m_counter++;
@@ -87,22 +90,8 @@ pair<environment, name> add_private_name(environment const & env, name const & n
     return mk_pair(new_env, r);
 }
 
-static unsigned mk_extra_hash_using_pos() {
-    unsigned h = 31;
-    if (auto pinfo = get_pos_info_provider()) {
-        h = hash(pinfo->get_some_pos().first, pinfo->get_some_pos().second);
-        char const * fname = pinfo->get_file_name();
-        h = hash_str(strlen(fname), fname, h);
-    }
-    return h;
-}
-
-pair<environment, name> mk_private_name(environment const & env, name const & c) {
-    return add_private_name(env, c, optional<unsigned>(mk_extra_hash_using_pos()));
-}
-
-pair<environment, name> mk_private_prefix(environment const & env, optional<unsigned> const & extra_hash) {
-    name r          = mk_private_name_core(env, name(), extra_hash);
+pair<environment, name> mk_private_prefix(environment const & env) {
+    name r          = mk_private_name_core(env, name());
     private_ext ext = get_extension(env);
     ext.m_private_prefixes.insert(r);
     ext.m_counter++;
@@ -110,10 +99,6 @@ pair<environment, name> mk_private_prefix(environment const & env, optional<unsi
     return mk_pair(new_env, r);
 }
 
-pair<environment, name> mk_private_prefix(environment const & env) {
-    return mk_private_prefix(env, optional<unsigned>(mk_extra_hash_using_pos()));
-}
-
 static optional<name> get_private_prefix(private_ext const & ext, name n) {
     while (true) {
         if (ext.m_private_prefixes.contains(n))
diff --git a/src/library/private.h b/src/library/private.h
index 3599f05d2d..c8753c8073 100644
--- a/src/library/private.h
+++ b/src/library/private.h
@@ -10,17 +10,11 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 
 namespace lean {
+environment set_main_module_name(environment const & env, name const & mod_name);
 /**
-   \brief This is an auxiliary function used to simulate private declarations. Whenever we want to create a "private"
-   declaration, this module creates an internal "hidden" name that is not accessible to users.
-   In principle, users can access the internal names if they want by applying themselves the procedure used to create
-   the "hidden" names.
-
-   The optional \c base_hash can be used to influence the "hidden" name associated with \c n.
-
-   The mapping between \c n and the "hidden" name is saved  in the .olean files.
+   \brief This is an auxiliary function used to simulate private declarations.
 */
-pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & base_hash);
+pair<environment, name> add_private_name(environment const & env, name const & n);
 
 /**
     \brief Return the user name associated with the hidden name \c n.
@@ -32,18 +26,14 @@ optional<name> hidden_to_user_name(environment const & env, name const & n);
 
 bool is_private(environment const & env, name const & n);
 
-pair<environment, name> mk_private_prefix(environment const & env, name const & n, optional<unsigned> const & base_hash);
+/* Create a private prefix that is going to be use to generate many private names.
+   This function registers the private prefix in the environment. */
+pair<environment, name> mk_private_prefix(environment const & env);
+pair<environment, name> mk_private_prefix(environment const & env, name const & n);
 
 /* Create a private name based on \c c and get_pos_info_provider(), and register it using \c add_private_name */
 pair<environment, name> mk_private_name(environment const & env, name const & c);
 
-/* Create a private prefix that is going to be use to generate many private names.
-   This function registers the private prefix in the environment. */
-pair<environment, name> mk_private_prefix(environment const & env, optional<unsigned> const & extra_hash);
-
-/* Similar to the previous function, but generate an extra_hash using get_pos_info_provider */
-pair<environment, name> mk_private_prefix(environment const & env);
-
 /* Register a \c n as the name for private name \c prv_n. \c prv_n must have been constructed using
    a prefix returned by \c mk_private_prefix. */
 environment register_private_name(environment const & env, name const & n, name const & prv_n);
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 4d0aef5d5e..0da7ae53c9 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -34,6 +34,7 @@ Author: Leonardo de Moura
 #include "library/io_state_stream.h"
 #include "library/message_builder.h"
 #include "library/time_task.h"
+#include "library/private.h"
 #include "library/compiler/emit_cpp.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/pp.h"
@@ -451,6 +452,7 @@ int main(int argc, char ** argv) {
         std::stringstream buf;
         buf << std::cin.rdbuf();
         contents = buf.str();
+        env      = set_main_module_name(env, "_stdin");
     } else {
         if (argc - optind != 1) {
             std::cerr << "Expected exactly one file name\n";
@@ -459,6 +461,7 @@ int main(int argc, char ** argv) {
         }
         mod_fn = lrealpath(argv[optind]);
         contents = read_file(mod_fn);
+        env      = set_main_module_name(env, module_name_of_file(path.get_path(), mod_fn));
     }
     try {
         message_log l;