diff --git a/stage0/src/Lean/Modifiers.lean b/stage0/src/Lean/Modifiers.lean
index 66d926c28f..5d0ccd0d2b 100644
--- a/stage0/src/Lean/Modifiers.lean
+++ b/stage0/src/Lean/Modifiers.lean
@@ -17,34 +17,19 @@ def addProtected (env : Environment) (n : Name) : Environment :=
 def isProtected (env : Environment) (n : Name) : Bool :=
   protectedExt.isTagged env n
 
-builtin_initialize privateExt : EnvExtension Nat ← registerEnvExtension (pure 1)
-
 /- Private name support.
 
    Suppose the user marks as declaration `n` as private. Then, we create
-   the name: `_private.<module_name>.<index> ++ n`.
-   We say `_private.<module_name>.<index>` is the "private prefix"
-   where `<index>` comes from the environment extension `privateExt`.
+   the name: `_private.<module_name>.0 ++ n`.
+   We say `_private.<module_name>.0` is the "private prefix"
 
    We assume that `n` is a valid user name and does not contain
    `Name.num` constructors. Thus, we can easily convert from
-   private internal name to user given name.
+   private internal name to the user given name.
 -/
 
 def privateHeader : Name := `_private
 
-@[export lean_mk_private_prefix]
-def mkUniquePrivatePrefix (env : Environment) : Environment × Name :=
-  let idx := privateExt.getState env
-  let p   := Name.mkNum (privateHeader ++ env.mainModule) idx
-  let env := privateExt.setState env (idx+1)
-  (env, p)
-
-@[export lean_mk_private_name]
-def mkUniquePrivateName (env : Environment) (n : Name) : Environment × Name :=
-  let (env, p) := mkUniquePrivatePrefix env
-  (env, p ++ n)
-
 def mkPrivateName (env : Environment) (n : Name) : Name :=
   Name.mkNum (privateHeader ++ env.mainModule) 0 ++ n
 
diff --git a/stage0/stdlib/Lean/Modifiers.c b/stage0/stdlib/Lean/Modifiers.c
index b2b98ae616..bfa8445513 100644
--- a/stage0/stdlib/Lean/Modifiers.c
+++ b/stage0/stdlib/Lean/Modifiers.c
@@ -18,10 +18,7 @@ lean_object* l_Lean_protectedExt___closed__1;
 lean_object* l_Lean_protectedExt___closed__3;
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_protectedExt___closed__5;
-lean_object* l_Lean_initFn____x40_Lean_Modifiers___hyg_30____closed__1;
 lean_object* l_Lean_privateHeader;
-lean_object* lean_mk_private_name(lean_object*, lean_object*);
-lean_object* l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(lean_object*, lean_object*);
 extern lean_object* l_Array_empty___closed__1;
 uint8_t lean_name_eq(lean_object*, lean_object*);
 lean_object* l_Lean_initFn____x40_Lean_Modifiers___hyg_3____closed__1;
@@ -32,22 +29,16 @@ uint8_t lean_is_private_name(lean_object*);
 lean_object* l_Lean_isPrivateName___boxed(lean_object*);
 lean_object* l_Lean_initFn____x40_Lean_Modifiers___hyg_3____closed__2;
 uint8_t l_Lean_isPrivateName(lean_object*);
-lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Lean_initFn____x40_Lean_Modifiers___hyg_3_(lean_object*);
-lean_object* l_Lean_initFn____x40_Lean_Modifiers___hyg_30_(lean_object*);
 lean_object* l___private_Lean_Modifiers_0__Lean_privateToUserNameAux_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_protectedExt___elambda__3___boxed(lean_object*, lean_object*);
 lean_object* lean_add_protected(lean_object*, lean_object*);
 extern lean_object* l_IO_instInhabitedError___closed__1;
-lean_object* lean_mk_private_prefix(lean_object*);
 lean_object* l_Lean_protectedExt;
-lean_object* l_Lean_mkUniquePrivateName_match__1___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_mkUniquePrivateName_match__1(lean_object*);
 lean_object* l_Lean_isPrivateName_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_protectedExt___elambda__2(lean_object*);
 lean_object* lean_private_prefix(lean_object*);
-lean_object* l_Lean_EnvExtensionInterfaceUnsafe_setState___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Modifiers_0__Lean_privateToUserNameAux_match__1(lean_object*);
 lean_object* l_Lean_isPrivateName_match__1(lean_object*);
 lean_object* l_Lean_isPrivateNameExport___boxed(lean_object*);
@@ -59,7 +50,6 @@ extern lean_object* l_Lean_EnvExtensionInterfaceUnsafe_instInhabitedExt___closed
 lean_object* l___private_Lean_Modifiers_0__Lean_privatePrefixAux(lean_object*);
 lean_object* l_Lean_protectedExt___elambda__3(lean_object*, lean_object*);
 lean_object* l_Lean_protectedExt___elambda__4___boxed(lean_object*, lean_object*);
-lean_object* l_Lean_privateExt;
 lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* l_Lean_mkTagDeclarationExtension(lean_object*, lean_object*);
 uint8_t l_Lean_TagDeclarationExtension_isTagged(lean_object*, lean_object*, lean_object*);
@@ -67,9 +57,7 @@ lean_object* l_Lean_protectedExt___elambda__4___rarg(lean_object*);
 lean_object* l_Lean_isProtected___boxed(lean_object*, lean_object*);
 lean_object* l___private_Lean_Modifiers_0__Lean_privatePrefixAux___boxed(lean_object*);
 lean_object* l_Lean_protectedExt___elambda__1(lean_object*);
-lean_object* l_EStateM_pure___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_privateHeader___closed__2;
-lean_object* l_Lean_EnvExtensionInterfaceUnsafe_getState___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_protectedExt___elambda__4(lean_object*, lean_object*);
 lean_object* l_Lean_protectedExt___closed__4;
 lean_object* l_Lean_privateHeader___closed__1;
@@ -262,25 +250,6 @@ x_4 = lean_box(x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_Lean_initFn____x40_Lean_Modifiers___hyg_30____closed__1() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; 
-x_1 = lean_unsigned_to_nat(1u);
-x_2 = lean_alloc_closure((void*)(l_EStateM_pure___rarg), 2, 1);
-lean_closure_set(x_2, 0, x_1);
-return x_2;
-}
-}
-lean_object* l_Lean_initFn____x40_Lean_Modifiers___hyg_30_(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; lean_object* x_3; 
-x_2 = l_Lean_initFn____x40_Lean_Modifiers___hyg_30____closed__1;
-x_3 = l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(x_2, x_1);
-return x_3;
-}
-}
 static lean_object* _init_l_Lean_privateHeader___closed__1() {
 _start:
 {
@@ -307,81 +276,6 @@ x_1 = l_Lean_privateHeader___closed__2;
 return x_1;
 }
 }
-lean_object* lean_mk_private_prefix(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
-x_2 = l_Lean_privateExt;
-x_3 = l_Lean_EnvExtensionInterfaceUnsafe_getState___rarg(x_2, x_1);
-lean_inc(x_1);
-x_4 = lean_environment_main_module(x_1);
-x_5 = l_Lean_privateHeader;
-x_6 = l_Lean_Name_append(x_5, x_4);
-lean_inc(x_3);
-x_7 = lean_name_mk_numeral(x_6, x_3);
-x_8 = lean_unsigned_to_nat(1u);
-x_9 = lean_nat_add(x_3, x_8);
-lean_dec(x_3);
-x_10 = l_Lean_EnvExtensionInterfaceUnsafe_setState___rarg(x_2, x_1, x_9);
-x_11 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_11, 0, x_10);
-lean_ctor_set(x_11, 1, x_7);
-return x_11;
-}
-}
-lean_object* l_Lean_mkUniquePrivateName_match__1___rarg(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; lean_object* x_4; lean_object* x_5; 
-x_3 = lean_ctor_get(x_1, 0);
-lean_inc(x_3);
-x_4 = lean_ctor_get(x_1, 1);
-lean_inc(x_4);
-lean_dec(x_1);
-x_5 = lean_apply_2(x_2, x_3, x_4);
-return x_5;
-}
-}
-lean_object* l_Lean_mkUniquePrivateName_match__1(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Lean_mkUniquePrivateName_match__1___rarg), 2, 0);
-return x_2;
-}
-}
-lean_object* lean_mk_private_name(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; uint8_t x_4; 
-x_3 = lean_mk_private_prefix(x_1);
-x_4 = !lean_is_exclusive(x_3);
-if (x_4 == 0)
-{
-lean_object* x_5; lean_object* x_6; 
-x_5 = lean_ctor_get(x_3, 1);
-x_6 = l_Lean_Name_append(x_5, x_2);
-lean_dec(x_5);
-lean_ctor_set(x_3, 1, x_6);
-return x_3;
-}
-else
-{
-lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
-x_7 = lean_ctor_get(x_3, 0);
-x_8 = lean_ctor_get(x_3, 1);
-lean_inc(x_8);
-lean_inc(x_7);
-lean_dec(x_3);
-x_9 = l_Lean_Name_append(x_8, x_2);
-lean_dec(x_8);
-x_10 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_10, 0, x_7);
-lean_ctor_set(x_10, 1, x_9);
-return x_10;
-}
-}
-}
 lean_object* l_Lean_mkPrivateName(lean_object* x_1, lean_object* x_2) {
 _start:
 {
@@ -675,13 +569,6 @@ if (lean_io_result_is_error(res)) return res;
 l_Lean_protectedExt = lean_io_result_get_value(res);
 lean_mark_persistent(l_Lean_protectedExt);
 lean_dec_ref(res);
-l_Lean_initFn____x40_Lean_Modifiers___hyg_30____closed__1 = _init_l_Lean_initFn____x40_Lean_Modifiers___hyg_30____closed__1();
-lean_mark_persistent(l_Lean_initFn____x40_Lean_Modifiers___hyg_30____closed__1);
-res = l_Lean_initFn____x40_Lean_Modifiers___hyg_30_(lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-l_Lean_privateExt = lean_io_result_get_value(res);
-lean_mark_persistent(l_Lean_privateExt);
-lean_dec_ref(res);
 l_Lean_privateHeader___closed__1 = _init_l_Lean_privateHeader___closed__1();
 lean_mark_persistent(l_Lean_privateHeader___closed__1);
 l_Lean_privateHeader___closed__2 = _init_l_Lean_privateHeader___closed__2();