diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 82d7d090c4..58954ba076 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1527,8 +1527,7 @@ struct to_pattern_fn {
         buffer<expr> args;
         get_app_args(e, args);
         args[0] = fix_quoted_name(args[0]);
-//        return mk_app(mk_constant(get_lean_name_str_name()), args);
-        return mk_app(mk_constant(name{"Lean", "Name", "mkString"}), args);
+        return mk_app(mk_constant(get_lean_name_str_name()), args);
     }
 
     expr fix_quoted_names(expr const & e) {
diff --git a/stage0/library/Init/Lean/AuxRecursor.c b/stage0/library/Init/Lean/AuxRecursor.c
index 283a0b5d5f..a13929f722 100644
--- a/stage0/library/Init/Lean/AuxRecursor.c
+++ b/stage0/library/Init/Lean/AuxRecursor.c
@@ -33,9 +33,9 @@ lean_object* l_Lean_noConfusionExt___elambda__4___boxed(lean_object*);
 lean_object* l_Lean_noConfusionExt___elambda__4___rarg(lean_object*);
 lean_object* l_Lean_noConfusionExt___elambda__2(lean_object*);
 lean_object* l_Lean_auxRecExt___elambda__1(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_auxRecExt___elambda__3(lean_object*, lean_object*);
 lean_object* l_Lean_auxRecExt___elambda__2(lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_noConfusionExt___elambda__1(lean_object*);
 lean_object* l_Lean_mkAuxRecursorExtension___closed__1;
 lean_object* l_Lean_mkAuxRecursorExtension(lean_object*);
diff --git a/stage0/library/Init/Lean/Class.c b/stage0/library/Init/Lean/Class.c
index a99476dda9..c59713a3fe 100644
--- a/stage0/library/Init/Lean/Class.c
+++ b/stage0/library/Init/Lean/Class.c
@@ -132,6 +132,7 @@ lean_object* l_Lean_hasOutParams___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_SMap_contains___at_Lean_isClass___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_SMap_empty___at_Lean_ClassState_Inhabited___spec__1___closed__1;
 size_t lean_name_hash_usize(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_ClassState_addEntry___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_Lean_ClassState_switch(lean_object*);
@@ -163,7 +164,6 @@ extern lean_object* l_Char_HasRepr___closed__1;
 uint8_t l_Lean_SMap_contains___at_Lean_isInstance___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_addClass___closed__3;
 lean_object* l_Lean_classExtension___elambda__3___boxed(lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_mkClassExtension___closed__1;
 lean_object* lean_nat_add(lean_object*, lean_object*);
 extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;
diff --git a/stage0/library/Init/Lean/Compiler/ClosedTermCache.c b/stage0/library/Init/Lean/Compiler/ClosedTermCache.c
index 0ee38c1633..6a1d9e9bba 100644
--- a/stage0/library/Init/Lean/Compiler/ClosedTermCache.c
+++ b/stage0/library/Init/Lean/Compiler/ClosedTermCache.c
@@ -68,6 +68,7 @@ lean_object* l_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_objec
 lean_object* l_Array_iterateMAux___main___at_Lean_mkClosedTermCacheExtension___spec__16(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at_Lean_mkClosedTermCacheExtension___spec__21___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkClosedTermCacheExtension___closed__5;
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_insert___at_Lean_mkClosedTermCacheExtension___spec__2(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 uint8_t lean_expr_eqv(lean_object*, lean_object*);
@@ -82,7 +83,6 @@ lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkClosedTermCacheExtens
 lean_object* l_Lean_SMap_empty___at_Lean_mkClosedTermCacheExtension___spec__12___closed__2;
 lean_object* l_HashMapImp_moveEntries___main___at_Lean_mkClosedTermCacheExtension___spec__9(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkClosedTermCacheExtension___closed__4;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_mkClosedTermCacheExtension___spec__15___boxed(lean_object*, lean_object*);
 lean_object* l_AssocList_find___main___at_Lean_getClosedTermName___spec__6___boxed(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Compiler/ConstFolding.c b/stage0/library/Init/Lean/Compiler/ConstFolding.c
index df03069d06..6a991e59ab 100644
--- a/stage0/library/Init/Lean/Compiler/ConstFolding.c
+++ b/stage0/library/Init/Lean/Compiler/ConstFolding.c
@@ -126,6 +126,7 @@ lean_object* l_Lean_Compiler_foldUIntDiv___lambda__1(lean_object*, uint8_t, lean
 lean_object* l_Lean_Compiler_natFoldFns___closed__7;
 lean_object* l_Lean_Compiler_foldBinOp___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_foldr___main___at_Lean_Compiler_isOfNat___spec__1___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_foldNatDecEq___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_natFoldFns___closed__3;
 lean_object* l_Lean_Compiler_numScalarTypes___closed__8;
@@ -174,7 +175,6 @@ uint8_t l_List_foldr___main___at_Lean_Compiler_isOfNat___spec__1(lean_object*, u
 lean_object* l_Lean_Compiler_mkUInt32Lit(lean_object*);
 lean_object* l_Lean_Compiler_foldNatDecLe(uint8_t, lean_object*, lean_object*);
 lean_object* l_List_append___rarg(lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_foldNatPow(uint8_t);
 lean_object* l_Lean_Compiler_boolFoldFns___closed__5;
 lean_object* l_Lean_Compiler_natFoldFns___closed__10;
diff --git a/stage0/library/Init/Lean/Compiler/ExportAttr.c b/stage0/library/Init/Lean/Compiler/ExportAttr.c
index 56afa32286..e07457b787 100644
--- a/stage0/library/Init/Lean/Compiler/ExportAttr.c
+++ b/stage0/library/Init/Lean/Compiler/ExportAttr.c
@@ -50,6 +50,7 @@ extern lean_object* l_Lean_AttributeImpl_inhabited___closed__4;
 lean_object* l_Lean_registerTagAttribute___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_String_anyAux___main___at___private_Init_Lean_Compiler_ExportAttr_1__isValidCppId___spec__2(uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkExportAttr___closed__1;
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___lambda__1___boxed(lean_object*);
@@ -62,7 +63,6 @@ uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___lambda__1(lean_object*);
 extern lean_object* l_Lean_ParametricAttribute_Inhabited___closed__1;
 lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkExportAttr___spec__7(lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;
 lean_object* l_Lean_PersistentEnvExtension_getModuleEntries___rarg(lean_object*, lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Compiler/ExternAttr.c b/stage0/library/Init/Lean/Compiler/ExternAttr.c
index e136e4782d..414e2605d0 100644
--- a/stage0/library/Init/Lean/Compiler/ExternAttr.c
+++ b/stage0/library/Init/Lean/Compiler/ExternAttr.c
@@ -72,6 +72,7 @@ extern lean_object* l_Lean_AttributeImpl_inhabited___closed__4;
 lean_object* l_Lean_registerTagAttribute___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_String_Iterator_next(lean_object*);
 lean_object* l_RBNode_find___main___at_Lean_getExternAttrData___spec__2(lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_ExternEntry_backend___boxed(lean_object*);
@@ -97,7 +98,6 @@ extern lean_object* l_Lean_ParametricAttribute_Inhabited___closed__1;
 lean_object* l_Lean_expandExternPatternAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Environment_isProjectionFn(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Compiler_ExternAttr_3__parseOptNum___main(lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Compiler_ExternAttr_1__syntaxToExternEntries___main___closed__2;
 lean_object* l___private_Init_Lean_Compiler_ExternAttr_2__syntaxToExternAttrData___closed__5;
 lean_object* lean_nat_add(lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Compiler/IR/Basic.c b/stage0/library/Init/Lean/Compiler/IR/Basic.c
index 190df7c061..0af6f3932c 100644
--- a/stage0/library/Init/Lean/Compiler/IR/Basic.c
+++ b/stage0/library/Init/Lean/Compiler/IR/Basic.c
@@ -101,6 +101,7 @@ lean_object* l_Lean_IR_Decl_isExtern___boxed(lean_object*);
 lean_object* l_Lean_IR_Arg_alphaEqv___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_RBNode_ins___main___at_Lean_IR_LocalContext_addLocal___spec__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_LocalContext_addJP(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at_Lean_IR_mmodifyJPs___spec__1___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_AltCore_body(lean_object*);
 lean_object* l_Lean_IR_AltCore_mmodifyBody___rarg(lean_object*, lean_object*, lean_object*);
@@ -132,7 +133,6 @@ lean_object* l_Lean_IR_LocalContext_eraseJoinPointDecl(lean_object*, lean_object
 lean_object* l_Lean_IR_Decl_name___boxed(lean_object*);
 lean_object* l_Lean_IR_mkIf___closed__7;
 lean_object* l_Lean_IR_LitVal_beq___boxed(lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_IR_mkIf___closed__2;
 lean_object* l_RBNode_appendTrees___main___rarg(lean_object*, lean_object*);
 lean_object* lean_ir_mk_ret(lean_object*);
diff --git a/stage0/library/Init/Lean/Compiler/IR/Boxing.c b/stage0/library/Init/Lean/Compiler/IR/Boxing.c
index afdec98662..61dccd2f75 100644
--- a/stage0/library/Init/Lean/Compiler/IR/Boxing.c
+++ b/stage0/library/Init/Lean/Compiler/IR/Boxing.c
@@ -58,6 +58,7 @@ lean_object* l_Lean_IR_ExplicitBoxing_castArgsIfNeededAux___at_Lean_IR_ExplicitB
 lean_object* l_Lean_IR_ExplicitBoxing_unboxResultIfNeeded___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_findEnvDecl_x27(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_LocalContext_addJP(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Nat_foldMAux___main___at_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_Monad___rarg(lean_object*);
 lean_object* l_Lean_IR_reshape(lean_object*, lean_object*);
@@ -78,7 +79,6 @@ lean_object* l_Lean_IR_ExplicitBoxing_castResultIfNeeded(lean_object*, lean_obje
 lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
 uint8_t l_Lean_IR_ExplicitBoxing_eqvTypes(lean_object*, lean_object*);
 lean_object* l_Lean_IR_ExplicitBoxing_getVarType(lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_IR_ExplicitBoxing_mkCast___closed__1;
 lean_object* l_Lean_IR_ExplicitBoxing_mkBoxedVersionAux(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Compiler/IR/CompilerM.c b/stage0/library/Init/Lean/Compiler/IR/CompilerM.c
index 364de62a18..7a6e57d1a8 100644
--- a/stage0/library/Init/Lean/Compiler/IR/CompilerM.c
+++ b/stage0/library/Init/Lean/Compiler/IR/CompilerM.c
@@ -93,6 +93,7 @@ lean_object* l_Lean_IR_mkDeclMapExtension(lean_object*);
 lean_object* l_Lean_IR_tracePrefixOptionName;
 lean_object* l_PersistentHashMap_find___at_Lean_IR_findEnvDecl___spec__2(lean_object*, lean_object*);
 size_t lean_name_hash_usize(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 uint8_t l_PersistentHashMap_contains___at_Lean_IR_containsDecl___spec__3(lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_IR_LogEntry_fmt___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -121,7 +122,6 @@ lean_object* l_Lean_IR_mkDeclMapExtension___lambda__2(lean_object*);
 lean_object* l_Lean_IR_declMapExt;
 lean_object* l_Array_iterateMAux___main___at_Lean_IR_mkDeclMapExtension___spec__9(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_IR_mkDeclMapExtension___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_IR_declMapExt___elambda__2(lean_object*);
 lean_object* l_Lean_IR_LogEntry_Lean_HasFormat;
 lean_object* l_Lean_IR_findDecl___boxed(lean_object*, lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Compiler/IR/Default.c b/stage0/library/Init/Lean/Compiler/IR/Default.c
index 8e59ff7f8c..a2581cb0e4 100644
--- a/stage0/library/Init/Lean/Compiler/IR/Default.c
+++ b/stage0/library/Init/Lean/Compiler/IR/Default.c
@@ -48,6 +48,7 @@ lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___closed__2
 extern lean_object* l_Lean_IR_tracePrefixOptionName;
 lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___closed__28;
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Compiler_IR_Default_1__compileAux___spec__5(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___closed__4;
@@ -56,7 +57,6 @@ uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l_Lean_IR_inferBorrow(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_Decl_elimDead(lean_object*);
 extern lean_object* l_Lean_IR_declMapExt;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Array_forMAux___main___at_Lean_IR_addBoxedVersionAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___closed__19;
diff --git a/stage0/library/Init/Lean/Compiler/IR/ElimDeadBranches.c b/stage0/library/Init/Lean/Compiler/IR/ElimDeadBranches.c
index d8a5c3586c..9d540f0756 100644
--- a/stage0/library/Init/Lean/Compiler/IR/ElimDeadBranches.c
+++ b/stage0/library/Init/Lean/Compiler/IR/ElimDeadBranches.c
@@ -121,6 +121,7 @@ uint8_t l_List_foldr___main___at_Lean_IR_UnreachableBranches_Value_beq___main___
 uint8_t l_Lean_IR_UnreachableBranches_containsCtor___main(lean_object*, lean_object*);
 lean_object* l_Lean_IR_UnreachableBranches_elimDead___boxed(lean_object*, lean_object*);
 size_t lean_name_hash_usize(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_AssocList_contains___main___at_Lean_IR_UnreachableBranches_mkFunctionSummariesExtension___spec__7___boxed(lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_Lean_IR_UnreachableBranches_updateVarAssignment___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -157,7 +158,6 @@ lean_object* l_AssocList_replace___main___at_Lean_IR_UnreachableBranches_mkFunct
 lean_object* l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__1;
 lean_object* l_PersistentArray_modify___at_Lean_IR_UnreachableBranches_updateCurrFnSummary___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_getPrefix(lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_mkHashMap___at_Lean_IR_UnreachableBranches_mkFunctionSummariesExtension___spec__13(lean_object*);
 lean_object* l_AssocList_find___main___at_Lean_IR_UnreachableBranches_findVarValue___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_IR_UnreachableBranches_functionSummariesExt___closed__4;
diff --git a/stage0/library/Init/Lean/Compiler/IR/EmitC.c b/stage0/library/Init/Lean/Compiler/IR/EmitC.c
index 554d86ef82..d6721ef7ef 100644
--- a/stage0/library/Init/Lean/Compiler/IR/EmitC.c
+++ b/stage0/library/Init/Lean/Compiler/IR/EmitC.c
@@ -217,6 +217,7 @@ lean_object* l_Lean_IR_mkVarJPMaps(lean_object*);
 lean_object* l_Lean_IR_EmitC_emitNumLit___closed__1;
 lean_object* l_Lean_IR_EmitC_toStringArgs___boxed(lean_object*);
 lean_object* l_Lean_IR_EmitC_emitInitFn(lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Nat_forMAux___main___at_Lean_IR_EmitC_emitTailCall___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_AltCore_body(lean_object*);
 lean_object* l_Lean_IR_EmitC_emitMainFn(lean_object*, lean_object*);
@@ -284,7 +285,6 @@ lean_object* l_Lean_IR_EmitC_emitArg(lean_object*, lean_object*, lean_object*);
 lean_object* l_List_foldl___main___at_Lean_IR_EmitC_emitFnDecls___spec__1___boxed(lean_object*, lean_object*);
 extern lean_object* l_Lean_IR_declMapExt;
 lean_object* l_Lean_IR_EmitC_emitCtorScalarSize___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_IR_EmitC_emitMainFn___closed__29;
 lean_object* l_Lean_IR_EmitC_emitMainFn___closed__39;
 extern lean_object* l_Char_quoteCore___closed__5;
diff --git a/stage0/library/Init/Lean/Compiler/IR/UnboxResult.c b/stage0/library/Init/Lean/Compiler/IR/UnboxResult.c
index 1ef56db98b..f039e15dda 100644
--- a/stage0/library/Init/Lean/Compiler/IR/UnboxResult.c
+++ b/stage0/library/Init/Lean/Compiler/IR/UnboxResult.c
@@ -23,8 +23,8 @@ lean_object* l_Lean_IR_UnboxResult_mkUnboxAttr___lambda__1___closed__5;
 lean_object* l_Lean_IR_UnboxResult_mkUnboxAttr___lambda__1___closed__7;
 lean_object* l_Lean_IR_UnboxResult_mkUnboxAttr___lambda__1___closed__6;
 lean_object* l_Lean_registerTagAttribute(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_IR_UnboxResult_mkUnboxAttr(lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
+lean_object* l_Lean_IR_UnboxResult_mkUnboxAttr(lean_object*);
 lean_object* l_Lean_IR_UnboxResult_mkUnboxAttr___closed__2;
 lean_object* l_Lean_IR_UnboxResult_mkUnboxAttr___lambda__1___closed__4;
 uint8_t l_Lean_TagAttribute_hasTag(lean_object*, lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Compiler/ImplementedByAttr.c b/stage0/library/Init/Lean/Compiler/ImplementedByAttr.c
index acd91e4dad..d246325932 100644
--- a/stage0/library/Init/Lean/Compiler/ImplementedByAttr.c
+++ b/stage0/library/Init/Lean/Compiler/ImplementedByAttr.c
@@ -45,6 +45,7 @@ lean_object* l_Lean_registerTagAttribute___lambda__5___boxed(lean_object*, lean_
 lean_object* l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1___lambda__1___boxed(lean_object*);
 lean_object* l_Lean_registerParametricAttribute___at_Lean_Compiler_mkImplementedByAttr___spec__1___lambda__1(lean_object*);
 lean_object* l_Lean_Compiler_mkImplementedByAttr___lambda__1(lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 uint8_t lean_expr_eqv(lean_object*, lean_object*);
 lean_object* l_Array_binSearchAux___main___at_Lean_Compiler_getImplementedBy___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -58,7 +59,6 @@ uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_mkImplementedByAttr___lambda__1___closed__1;
 extern lean_object* l_Char_HasRepr___closed__1;
 extern lean_object* l_Lean_ParametricAttribute_Inhabited___closed__1;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_mkImplementedByAttr___closed__3;
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_mkImplementedByAttr___lambda__2(lean_object*, lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Compiler/InitAttr.c b/stage0/library/Init/Lean/Compiler/InitAttr.c
index 80be9352ea..694fcada94 100644
--- a/stage0/library/Init/Lean/Compiler/InitAttr.c
+++ b/stage0/library/Init/Lean/Compiler/InitAttr.c
@@ -58,6 +58,7 @@ lean_object* l_Lean_initAttr;
 lean_object* l_RBNode_fold___main___at_Lean_mkInitAttr___spec__2(lean_object*, lean_object*);
 uint8_t l_Lean_hasInitAttr(lean_object*, lean_object*);
 lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_mkInitAttr___spec__5(lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 uint8_t lean_expr_eqv(lean_object*, lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
@@ -69,7 +70,6 @@ extern lean_object* l_Lean_registerParametricAttribute___rarg___closed__2;
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 extern lean_object* l_Char_HasRepr___closed__1;
 extern lean_object* l_Lean_ParametricAttribute_Inhabited___closed__1;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_mkInitAttr___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;
diff --git a/stage0/library/Init/Lean/Compiler/InlineAttrs.c b/stage0/library/Init/Lean/Compiler/InlineAttrs.c
index f934529af3..94b1183a53 100644
--- a/stage0/library/Init/Lean/Compiler/InlineAttrs.c
+++ b/stage0/library/Init/Lean/Compiler/InlineAttrs.c
@@ -63,6 +63,7 @@ lean_object* l_Lean_Compiler_mkInlineAttrs___lambda__1(lean_object*, lean_object
 lean_object* l_Lean_Compiler_mkInlineAttrs___closed__17;
 lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_Compiler_mkInlineAttrs___spec__4___closed__1;
 lean_object* l_List_forM___main___at_Lean_registerEnumAttributes___spec__11(lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Environment_getModuleIdxFor(lean_object*, lean_object*);
@@ -83,7 +84,6 @@ lean_object* l_Lean_Compiler_mkInlineAttrs___closed__2;
 lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_getPrefix(lean_object*);
 lean_object* l_Lean_Compiler_mkInlineAttrs(lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_mkInlineAttrs___closed__4;
 lean_object* lean_nat_add(lean_object*, lean_object*);
 extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;
diff --git a/stage0/library/Init/Lean/Compiler/NeverExtractAttr.c b/stage0/library/Init/Lean/Compiler/NeverExtractAttr.c
index 5a116d2cfc..bbc0178fa6 100644
--- a/stage0/library/Init/Lean/Compiler/NeverExtractAttr.c
+++ b/stage0/library/Init/Lean/Compiler/NeverExtractAttr.c
@@ -17,9 +17,9 @@ lean_object* l_Lean_neverExtractAttr;
 extern lean_object* l_Lean_TagAttribute_Inhabited___closed__3;
 lean_object* l_Lean_hasNeverExtractAttribute___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_registerTagAttribute(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_mkNeverExtractAttr___lambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Name_getPrefix(lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_mkNeverExtractAttr___closed__2;
 lean_object* l___private_Init_Lean_Compiler_NeverExtractAttr_1__hasNeverExtractAttributeAux___boxed(lean_object*, lean_object*);
 uint8_t l_Lean_TagAttribute_hasTag(lean_object*, lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Compiler/Specialize.c b/stage0/library/Init/Lean/Compiler/Specialize.c
index 8123f313bc..3f831682eb 100644
--- a/stage0/library/Init/Lean/Compiler/Specialize.c
+++ b/stage0/library/Init/Lean/Compiler/Specialize.c
@@ -110,6 +110,7 @@ lean_object* l_List_forM___main___at_Lean_registerEnumAttributes___spec__11(lean
 lean_object* l_Lean_Compiler_specExtension;
 lean_object* l_Lean_Compiler_specExtension___closed__1;
 size_t lean_name_hash_usize(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_SMap_insert___at_Lean_Compiler_SpecState_addEntry___spec__12(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_Array_iterateMAux___main___at_Lean_Compiler_mkSpecExtension___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -142,7 +143,6 @@ lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_
 lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Compiler_mkSpecExtension___spec__7___closed__2;
 lean_object* l_Lean_SMap_insert___at_Lean_Compiler_SpecState_addEntry___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_Compiler_mkSpecializeAttrs___spec__5(lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_registerSimplePersistentEnvExtension___at_Lean_Compiler_mkSpecExtension___spec__4(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;
diff --git a/stage0/library/Init/Lean/Compiler/Util.c b/stage0/library/Init/Lean/Compiler/Util.c
index ab7396b3e4..92bf6f08a5 100644
--- a/stage0/library/Init/Lean/Compiler/Util.c
+++ b/stage0/library/Init/Lean/Compiler/Util.c
@@ -32,12 +32,12 @@ lean_object* l_Lean_Compiler_mkLcProof(lean_object*);
 lean_object* l_Lean_Compiler_objectType___closed__3;
 lean_object* l_Nat_repr(lean_object*);
 lean_object* l_Lean_Compiler_neutralExpr___closed__1;
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_objectType;
 lean_object* l_Lean_Compiler_neutralExpr___closed__3;
 lean_object* lean_string_append(lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_atMostOnce___closed__1;
 lean_object* l_Lean_Compiler_objectType___closed__2;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_atMostOnce_visit___main(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_atMostOnce___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_objectType___closed__1;
diff --git a/stage0/library/Init/Lean/Elaborator/Alias.c b/stage0/library/Init/Lean/Elaborator/Alias.c
index 582efc2ca2..2667198b46 100644
--- a/stage0/library/Init/Lean/Elaborator/Alias.c
+++ b/stage0/library/Init/Lean/Elaborator/Alias.c
@@ -73,6 +73,7 @@ lean_object* l_Lean_aliasExtension___elambda__4___boxed(lean_object*);
 lean_object* l_Lean_aliasExtension___closed__6;
 lean_object* l_Lean_addAlias(lean_object*, lean_object*, lean_object*);
 size_t lean_name_hash_usize(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_findAux___main___at_Lean_addAliasEntry___spec__3(lean_object*, size_t, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_Array_iterateMAux___main___at_Lean_mkAliasExtension___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -88,7 +89,6 @@ lean_object* l_HashMapImp_find___at_Lean_addAliasEntry___spec__5(lean_object*, l
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l_Lean_SMap_find___at_Lean_addAliasEntry___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_aliasExtension___closed__1;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_HashMapImp_moveEntries___main___at_Lean_addAliasEntry___spec__15(lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;
diff --git a/stage0/library/Init/Lean/Elaborator/Basic.c b/stage0/library/Init/Lean/Elaborator/Basic.c
index 8501ea5287..a2f2660215 100644
--- a/stage0/library/Init/Lean/Elaborator/Basic.c
+++ b/stage0/library/Init/Lean/Elaborator/Basic.c
@@ -27,6 +27,7 @@ lean_object* l_Lean_Elab_withInPattern___rarg(lean_object*, lean_object*, lean_o
 lean_object* l_Lean_Elab_toBaseDir(lean_object*, lean_object*);
 extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__4;
 lean_object* l_Lean_attrParamSyntaxToIdentifier(lean_object*);
+lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* l_AssocList_replace___main___at_Lean_addBuiltinTermElab___spec__16(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Name_beq___main(lean_object*, lean_object*);
 lean_object* l_Lean_ElabScope_Inhabited;
@@ -201,6 +202,7 @@ extern lean_object* l_Lean_NameGenerator_Inhabited___closed__3;
 lean_object* l_Lean_Elab_getNamespace(lean_object*);
 lean_object* l_Lean_Elab_logErrorAt___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 size_t lean_name_hash_usize(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_mkLocalDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_Lean_Elab_modifyScope___at_Lean_Elab_mkAnonymousInstName___spec__1___rarg(lean_object*);
@@ -248,7 +250,6 @@ lean_object* l_System_FilePath_dirName(lean_object*);
 lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
 lean_object* l_Lean_SMap_empty___at_Lean_mkBuiltinCommandElabTable___spec__1;
 lean_object* l_Lean_Elab_getUniverses___rarg(lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_resolveNamespaceUsingScopes___main(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_mkMessage(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_nameToExprAux___main(lean_object*);
@@ -341,7 +342,6 @@ lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkTermElabAttribute___s
 size_t lean_usize_modn(size_t, lean_object*);
 lean_object* l_Lean_ParametricAttribute_setParam___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_registerBuiltinTermElabAttr___lambda__1___closed__3;
-lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* l_Lean_ConstantInfo_type(lean_object*);
 lean_object* lean_environment_find(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_getElabContext(lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Elaborator/Command.c b/stage0/library/Init/Lean/Elaborator/Command.c
index 9d2c5002d4..aab81dc60d 100644
--- a/stage0/library/Init/Lean/Elaborator/Command.c
+++ b/stage0/library/Init/Lean/Elaborator/Command.c
@@ -118,6 +118,7 @@ lean_object* l_Lean_Elab_elabOpenRenaming(lean_object*, lean_object*, lean_objec
 extern lean_object* l_Lean_Parser_Command_mixfix___elambda__1___closed__2;
 extern lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__2;
 lean_object* l_Lean_addAlias(lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Command_universes___elambda__1___closed__2;
 lean_object* l_Lean_Elab_elabVariable___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_elabOpen___closed__1;
@@ -141,7 +142,6 @@ lean_object* l_Lean_Elab_elabExport(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Command_resolve__name___elambda__1___rarg___closed__2;
 extern lean_object* l_Lean_Parser_Command_notation___elambda__1___closed__2;
 lean_object* l_Lean_Elab_getUniverses___rarg(lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 extern lean_object* l_String_Iterator_HasRepr___closed__2;
 extern lean_object* l_Lean_Parser_Command_open___elambda__1___closed__2;
diff --git a/stage0/library/Init/Lean/Elaborator/ElabStrategyAttrs.c b/stage0/library/Init/Lean/Elaborator/ElabStrategyAttrs.c
index 4808f855b7..e72d4339e9 100644
--- a/stage0/library/Init/Lean/Elaborator/ElabStrategyAttrs.c
+++ b/stage0/library/Init/Lean/Elaborator/ElabStrategyAttrs.c
@@ -59,6 +59,7 @@ lean_object* l_Lean_registerTagAttribute___lambda__5___boxed(lean_object*, lean_
 extern lean_object* l_Lean_EnumAttributes_Inhabited___closed__1;
 lean_object* l_Lean_mkElaboratorStrategyAttrs___closed__15;
 lean_object* l_List_forM___main___at_Lean_registerEnumAttributes___spec__11(lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
 lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_mkElaboratorStrategyAttrs___spec__4___closed__1;
@@ -71,7 +72,6 @@ lean_object* l_Lean_mkElaboratorStrategyAttrs___closed__17;
 lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkElaboratorStrategyAttrs___spec__7(lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_mkElaboratorStrategyAttrs___lambda__1___closed__1;
 lean_object* l_Lean_mkElaboratorStrategyAttrs(lean_object*);
 lean_object* l_List_map___main___at_Lean_mkElaboratorStrategyAttrs___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Elaborator/PreTerm.c b/stage0/library/Init/Lean/Elaborator/PreTerm.c
index 46b1942a00..7ff3478d4a 100644
--- a/stage0/library/Init/Lean/Elaborator/PreTerm.c
+++ b/stage0/library/Init/Lean/Elaborator/PreTerm.c
@@ -124,6 +124,7 @@ lean_object* l_Lean_registerBuiltinPreTermElabAttr(lean_object*);
 lean_object* l_Lean_Elab_convertSort(lean_object*, lean_object*);
 lean_object* l_Lean_mkAsPattern(lean_object*, lean_object*);
 size_t lean_name_hash_usize(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_toPreTerm___closed__1;
 lean_object* l___private_Init_Lean_Elaborator_PreTerm_1__setPos___closed__3;
 lean_object* l_Lean_Elab_localContext___rarg(lean_object*);
@@ -157,7 +158,6 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_convertType___closed__4;
 lean_object* l_Lean_Syntax_getId___rarg(lean_object*);
 lean_object* l_Lean_mkFVar(lean_object*);
 lean_object* l_Lean_Elab_getUniverses___rarg(lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elaborator_PreTerm_5__processBinders(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_registerBuiltinPreTermElabAttr___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_convertProp(lean_object*);
diff --git a/stage0/library/Init/Lean/Elaborator/Term.c b/stage0/library/Init/Lean/Elaborator/Term.c
index 945f850e03..fd58c37c84 100644
--- a/stage0/library/Init/Lean/Elaborator/Term.c
+++ b/stage0/library/Init/Lean/Elaborator/Term.c
@@ -42,6 +42,7 @@ lean_object* l_Lean_Elab_mkExplicitBinder___rarg___closed__3;
 lean_object* l_Lean_Elab_elabListLit___closed__4;
 lean_object* l___regBuiltinTermElab_Lean_Elab_elabListLit(lean_object*);
 size_t lean_name_hash_usize(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabTermAux___main___closed__1;
 lean_object* l___regBuiltinTermElab_Lean_Elab_elabArrow___closed__1;
@@ -58,7 +59,6 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_elabArrow(lean_object*);
 lean_object* l_AssocList_find___main___at_Lean_Elab_elabTermAux___main___spec__6___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabListLit___closed__3;
 lean_object* l_Array_umapMAux___main___at_Lean_Elab_elabTermAux___main___spec__7(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabListLit___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_nullKind;
diff --git a/stage0/library/Init/Lean/Environment.c b/stage0/library/Init/Lean/Environment.c
index a5d530cbf6..d79c05cebb 100644
--- a/stage0/library/Init/Lean/Environment.c
+++ b/stage0/library/Init/Lean/Environment.c
@@ -195,6 +195,7 @@ lean_object* l_Lean_CPPExtensionState_inhabited;
 lean_object* l_Lean_Environment_displayStats___closed__1;
 lean_object* l_Lean_Environment_displayStats___closed__2;
 size_t lean_name_hash_usize(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_readModuleData___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_PersistentHashMap_foldlM___at_Lean_mkModuleData___spec__2___boxed(lean_object*, lean_object*);
@@ -250,7 +251,6 @@ lean_object* l_Lean_Environment_Inhabited___closed__3;
 lean_object* l_Lean_SimplePersistentEnvExtension_getEntries(lean_object*, lean_object*);
 lean_object* l_Lean_SimplePersistentEnvExtension_getState___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_namespacesExt___closed__4;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Environment_3__getTrustLevel___boxed(lean_object*);
 lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_regModListExtension___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg(lean_object*, lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/EqnCompiler/MatchPattern.c b/stage0/library/Init/Lean/EqnCompiler/MatchPattern.c
index 6666d63859..c597d7cd9d 100644
--- a/stage0/library/Init/Lean/EqnCompiler/MatchPattern.c
+++ b/stage0/library/Init/Lean/EqnCompiler/MatchPattern.c
@@ -21,9 +21,9 @@ lean_object* l_Lean_EqnCompiler_mkMatchPatternAttr(lean_object*);
 lean_object* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___closed__1;
 lean_object* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_registerTagAttribute(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_EqnCompiler_hasMatchPatternAttribute___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_EqnCompiler_mkMatchPatternAttr___closed__4;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 uint8_t l_Lean_TagAttribute_hasTag(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_EqnCompiler_mkMatchPatternAttr___closed__1;
 lean_object* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1(lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Expr.c b/stage0/library/Init/Lean/Expr.c
index 017d88a438..3b6d159daf 100644
--- a/stage0/library/Init/Lean/Expr.c
+++ b/stage0/library/Init/Lean/Expr.c
@@ -189,6 +189,7 @@ uint8_t l_Lean_BinderInfo_isAuxDecl(uint8_t);
 lean_object* l___private_Init_Lean_Expr_6__mkAppRevRangeAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_isMData___boxed(lean_object*);
 size_t lean_name_hash_usize(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Expr_updateForall_x21___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_Hashable___closed__1;
 uint8_t lean_expr_eqv(lean_object*, lean_object*);
@@ -245,7 +246,6 @@ lean_object* l_Lean_Literal_inhabited___closed__1;
 lean_object* l_Lean_mkDecIsFalse(lean_object*, lean_object*);
 lean_object* l_Lean_mkFVar(lean_object*);
 lean_object* l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__2;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_ExprStructEq_beq___boxed(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Expr_8__etaExpandedBody___main(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_HasRepr;
diff --git a/stage0/library/Init/Lean/Format.c b/stage0/library/Init/Lean/Format.c
index 09527b7bb9..19eda9b622 100644
--- a/stage0/library/Init/Lean/Format.c
+++ b/stage0/library/Init/Lean/Format.c
@@ -86,6 +86,7 @@ lean_object* l_Lean_Format_getUnicode___closed__1;
 lean_object* l_Lean_Format_joinArraySep(lean_object*);
 lean_object* l_Lean_toStringToFormat___rarg___closed__1;
 lean_object* l_Lean_fmt___at_Lean_arrayHasFormat___spec__1___rarg(lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_uint64HasFormat(uint64_t);
 lean_object* l_Lean_toStringToFormat___rarg___lambda__1(lean_object*);
 lean_object* l_Lean_Format_repr___main___closed__17;
@@ -115,7 +116,6 @@ lean_object* l_Lean_arrayHasFormat___rarg(lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_Format_joinArraySep___spec__1(lean_object*);
 lean_object* l_Lean_formatEntry(lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_Format_joinArraySep___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_natHasFormat(lean_object*);
 lean_object* l_Lean_Format_repr___main___closed__19;
 lean_object* l_Int_repr(lean_object*);
diff --git a/stage0/library/Init/Lean/Meta/Basic.c b/stage0/library/Init/Lean/Meta/Basic.c
index 2beff5cc71..7a42a3a621 100644
--- a/stage0/library/Init/Lean/Meta/Basic.c
+++ b/stage0/library/Init/Lean/Meta/Basic.c
@@ -25,6 +25,7 @@ lean_object* l_Lean_Meta_mkFreshLevelMVarId___boxed(lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getEnv___boxed(lean_object*);
 lean_object* l_Lean_Meta_usingAtLeastTransparency___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___main___at_Lean_Meta_forallTelescope___spec__1(lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_resettingTypeClassCache___rarg(lean_object*, lean_object*, lean_object*);
@@ -158,7 +159,6 @@ lean_object* l_Lean_Meta_throwBug(lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_8__forallTelescopeReducingAux(lean_object*);
 lean_object* l_Lean_Meta_usingTransparency___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkForall(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getExprMVarAssignment___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* lean_environment_find(lean_object*, lean_object*);
 size_t lean_usize_mix_hash(size_t, size_t);
diff --git a/stage0/library/Init/Lean/Meta/Default.c b/stage0/library/Init/Lean/Meta/Default.c
index 1367aa9dee..3d5678cddc 100644
--- a/stage0/library/Init/Lean/Meta/Default.c
+++ b/stage0/library/Init/Lean/Meta/Default.c
@@ -112,6 +112,7 @@ lean_object* l_Nat_foldMAux___main___at_Lean_Meta_getFunInfo___spec__2___boxed(l
 lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_getFunInfo___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_reduceRec___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___main___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__37(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_isClassExpensive___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__34(lean_object*, lean_object*, lean_object*);
 uint8_t lean_expr_eqv(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_WHNF_9__deltaBetaDefinition___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__23(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -140,7 +141,6 @@ lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_isProp___sp
 lean_object* l_Lean_mkFVar(lean_object*);
 lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___main___at_Lean_Meta_isProp___spec__9(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_reduceRec___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getConstAux(lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* lean_instantiate_value_lparams(lean_object*, lean_object*);
 uint8_t l_Lean_LocalDecl_binderInfo(lean_object*);
diff --git a/stage0/library/Init/Lean/Meta/ExprDefEq.c b/stage0/library/Init/Lean/Meta/ExprDefEq.c
index aa0f60ede2..c288cb6a6f 100644
--- a/stage0/library/Init/Lean/Meta/ExprDefEq.c
+++ b/stage0/library/Init/Lean/Meta/ExprDefEq.c
@@ -19,6 +19,7 @@ lean_object* l_Array_anyRangeMAux___main___at_Lean_Meta_CheckAssignment_checkFVa
 lean_object* l___private_Init_Lean_Meta_ExprDefEq_8__checkAssignmentFailure___closed__12;
 uint8_t l_Lean_Expr_hasFVar(lean_object*);
 lean_object* l___private_Init_Lean_Meta_ExprDefEq_4__isDefEqArgs___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 uint8_t l_Lean_Name_beq___main(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_CheckAssignment_checkMVar(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_ExprDefEq_14__processAssignmentAux___main___closed__4;
@@ -87,6 +88,7 @@ lean_object* l_Lean_Meta_isDefEqBindingDomain(lean_object*, lean_object*, lean_o
 lean_object* l___private_Init_Lean_Meta_ExprDefEq_3__isDefEqArgsAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_AssocList_find___main___at_Lean_Meta_CheckAssignment_findCached___spec__2(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_ExprDefEq_8__checkAssignmentFailure___closed__6;
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 uint8_t lean_expr_eqv(lean_object*, lean_object*);
 uint8_t l_Array_anyRangeMAux___main___at_Lean_Meta_checkAssignment___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkLambda(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -114,7 +116,6 @@ lean_object* l_Lean_mkFVar(lean_object*);
 lean_object* l___private_Init_Lean_Meta_ExprDefEq_8__checkAssignmentFailure___closed__21;
 lean_object* l_Lean_Meta_CheckAssignment_getMCtx___boxed(lean_object*);
 lean_object* l_Lean_Meta_CheckAssignment_check___main(lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_ExprDefEq_3__isDefEqArgsAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_isEtaUnassignedMVar___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
@@ -169,7 +170,6 @@ lean_object* l___private_Init_Lean_Expr_3__getAppArgsAux___main(lean_object*, le
 lean_object* l___private_Init_Lean_Meta_ExprDefEq_2__isDefEqArgsFirstPass___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 size_t lean_usize_modn(size_t, lean_object*);
 lean_object* l_Lean_LocalDecl_value_x3f(lean_object*);
-lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_LevelDefEq_13__restore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_CheckAssignment_checkFVar(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_ExprDefEq_5__isDefEqBindingAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Meta/LevelDefEq.c b/stage0/library/Init/Lean/Meta/LevelDefEq.c
index 67f9e0bfe0..9b07c7da09 100644
--- a/stage0/library/Init/Lean/Meta/LevelDefEq.c
+++ b/stage0/library/Init/Lean/Meta/LevelDefEq.c
@@ -45,6 +45,7 @@ lean_object* l___private_Init_Lean_Meta_LevelDefEq_7__isLevelDefEqAux___boxed(le
 lean_object* l___private_Init_Lean_Meta_LevelDefEq_7__isLevelDefEqAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_repr(lean_object*);
 lean_object* l___private_Init_Lean_Meta_LevelDefEq_6__getLevelConstraintKind___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_LevelDefEq_12__processPostponed___closed__2;
 extern lean_object* l_PersistentArray_empty___closed__3;
 lean_object* l___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep(lean_object*, lean_object*);
@@ -60,7 +61,6 @@ uint8_t l_Lean_Level_isSucc(lean_object*);
 lean_object* l_Lean_Level_dec___main(lean_object*);
 lean_object* l___private_Init_Lean_Meta_LevelDefEq_7__isLevelDefEqAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentArray_foldlM___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Meta_LevelDefEq_4__solveSelfMax___rarg(lean_object*, lean_object*, lean_object*);
 uint8_t l___private_Init_Lean_Meta_LevelDefEq_1__strictOccursMaxAux(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/MetavarContext.c b/stage0/library/Init/Lean/MetavarContext.c
index da7fd55572..df2f798bbd 100644
--- a/stage0/library/Init/Lean/MetavarContext.c
+++ b/stage0/library/Init/Lean/MetavarContext.c
@@ -34,6 +34,7 @@ lean_object* l___private_Init_Lean_MetavarContext_5__instantiateDelayedAux___mai
 lean_object* l___private_Init_Lean_MetavarContext_10__dep___main___at___private_Init_Lean_MetavarContext_13__collectDeps___spec__27___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_MkBinding_Exception_hasToString___closed__1;
 lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_MetavarContext_13__collectDeps___spec__46(lean_object*);
+lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 uint8_t l_Lean_Name_beq___main(lean_object*, lean_object*);
 lean_object* l_Nat_foldRevMAux___main___at_Lean_MetavarContext_mkBinding___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_findAux___main___at_Lean_MetavarContext_getLevelAssignment___spec__2(lean_object*, size_t, lean_object*);
@@ -360,7 +361,6 @@ size_t lean_usize_modn(size_t, lean_object*);
 lean_object* l_Lean_MetavarContext_Inhabited;
 lean_object* l_Lean_MetavarContext_mkBinding(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentArray_foldlMAux___main___at___private_Init_Lean_MetavarContext_13__collectDeps___spec__42(lean_object*);
-lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* l_PersistentArray_foldlFromM___at___private_Init_Lean_MetavarContext_13__collectDeps___spec__40(lean_object*);
 lean_object* l_Array_umapMAux___main___at_Lean_MetavarContext_MkBinding_Exception_toString___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_MetavarContext_13__collectDeps___spec__45___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Modifiers.c b/stage0/library/Init/Lean/Modifiers.c
index 9899229459..9c3952615a 100644
--- a/stage0/library/Init/Lean/Modifiers.c
+++ b/stage0/library/Init/Lean/Modifiers.c
@@ -15,6 +15,7 @@ extern "C" {
 #endif
 lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_namespacesExt___closed__1;
+lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 uint8_t l_Lean_Name_beq___main(lean_object*, lean_object*);
 lean_object* lean_environment_main_module(lean_object*);
 extern lean_object* l_Array_empty___closed__1;
@@ -40,13 +41,13 @@ lean_object* lean_io_initializing(lean_object*);
 lean_object* l_Lean_protectedExt___elambda__1(lean_object*);
 lean_object* l_Lean_mkPrivateExtension___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_mkProtectedExtension___closed__1;
 lean_object* l_Lean_protectedExt___closed__2;
 lean_object* l_Lean_privateExt___closed__1;
 lean_object* l___private_Init_Lean_Modifiers_2__privatePrefixAux(lean_object*);
 uint8_t l_Lean_isPrivateName___main(lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_protectedExt;
 lean_object* l_Lean_privateHeader;
 lean_object* lean_nat_add(lean_object*, lean_object*);
@@ -60,7 +61,6 @@ lean_object* l_Lean_protectedExt___elambda__3(lean_object*, lean_object*);
 lean_object* lean_mk_private_name(lean_object*, lean_object*);
 lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* lean_io_ref_get(lean_object*, lean_object*);
-lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* l_Lean_privateExt___elambda__1(lean_object*);
 uint8_t lean_is_protected(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
diff --git a/stage0/library/Init/Lean/Name.c b/stage0/library/Init/Lean/Name.c
index 985bae8fd5..c9eb1371f3 100644
--- a/stage0/library/Init/Lean/Name.c
+++ b/stage0/library/Init/Lean/Name.c
@@ -13,6 +13,7 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 uint8_t l_Lean_Name_beq___main(lean_object*, lean_object*);
 lean_object* l_Lean_Name_HasToString;
 lean_object* l_Lean_Name_toStringWithSep___main___closed__1;
@@ -24,7 +25,6 @@ lean_object* l_RBNode_find___main___at_Lean_NameMap_find___spec__1(lean_object*)
 lean_object* l_Lean_Name_quickLtAux___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_Hashable;
 lean_object* l_Lean_stringToName;
-lean_object* l_Lean_Name_mkNumeral___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_isPrefixOf___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_hasLtQuick;
 lean_object* l_Lean_Name_replacePrefix___boxed(lean_object*, lean_object*, lean_object*);
@@ -41,10 +41,8 @@ lean_object* l_Lean_Inhabited;
 uint8_t l_Lean_Name_isPrefixOf(lean_object*, lean_object*);
 lean_object* l_Lean_Name_quickLt___boxed(lean_object*, lean_object*);
 uint8_t l_Lean_Name_isAtomic(lean_object*);
-lean_object* l_Lean_mkSimpleName(lean_object*);
 lean_object* l_Lean_Name_getNumParts___boxed(lean_object*);
 lean_object* l_Lean_NameMap_find___rarg(lean_object*, lean_object*);
-lean_object* l_Lean_mkStrName(lean_object*, lean_object*);
 uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*);
 lean_object* l_Nat_repr(lean_object*);
 lean_object* l_Lean_mkNameStr(lean_object*, lean_object*);
@@ -52,6 +50,7 @@ lean_object* l_Lean_Name_append(lean_object*, lean_object*);
 lean_object* l_RBNode_insert___at_Lean_NameSet_insert___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkNameNum(lean_object*, lean_object*);
 size_t lean_name_hash_usize(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Name_HasAppend___closed__1;
 lean_object* l_Lean_Name_DecidableRel___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_append___main___boxed(lean_object*, lean_object*);
@@ -68,7 +67,7 @@ lean_object* l_Lean_NameSet_contains___boxed(lean_object*, lean_object*);
 lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_getPrefix(lean_object*);
 lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
+lean_object* l_Lean_Name_mkString(lean_object*, lean_object*);
 lean_object* l_Lean_mkNameSet;
 lean_object* lean_nat_add(lean_object*, lean_object*);
 uint8_t l_Lean_NameMap_contains___rarg(lean_object*, lean_object*);
@@ -103,8 +102,8 @@ lean_object* l_RBNode_find___main___at_Lean_NameMap_find___spec__1___rarg(lean_o
 uint8_t l_Lean_Name_lt(lean_object*, lean_object*);
 lean_object* l_Lean_Name_isAtomic___boxed(lean_object*);
 uint8_t l_Lean_Name_quickLt(lean_object*, lean_object*);
+lean_object* l_Lean_Name_num___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_appendAfter(lean_object*, lean_object*);
-lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* l_RBNode_ins___main___at_Lean_NameMap_insert___spec__2___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_String_toName(lean_object*);
 lean_object* l_Lean_Name_beq___main___boxed(lean_object*, lean_object*);
@@ -123,10 +122,10 @@ lean_object* l_Lean_Name_replacePrefix(lean_object*, lean_object*, lean_object*)
 lean_object* l_String_splitOn(lean_object*, lean_object*);
 uint8_t l_Lean_Name_isPrefixOf___main(lean_object*, lean_object*);
 lean_object* l_List_foldl___main___at_String_toName___spec__1___boxed(lean_object*, lean_object*);
+lean_object* l_Lean_mkNameSimple(lean_object*);
 lean_object* l_Lean_Name_lt___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_replacePrefix___main___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_HasAppend;
-lean_object* l_Lean_Name_mkString___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_NameSet_insert(lean_object*, lean_object*);
 lean_object* l_RBNode_find___main___at_Lean_NameMap_contains___spec__1___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_quickLtAux___main___boxed(lean_object*, lean_object*);
@@ -135,7 +134,6 @@ lean_object* l_Lean_NameMap_contains___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
 lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1(lean_object*);
 lean_object* l_Lean_Name_toStringWithSep___boxed(lean_object*, lean_object*);
-lean_object* l_Lean_mkNumName(lean_object*, lean_object*);
 lean_object* l_Lean_Name_HasToString___closed__1;
 uint8_t l_Lean_Name_isInternal(lean_object*);
 lean_object* l_Lean_Name_toString(lean_object*);
@@ -143,7 +141,8 @@ lean_object* l_RBNode_ins___main___at_Lean_NameSet_insert___spec__2(lean_object*
 lean_object* l_RBNode_ins___main___at_Lean_NameMap_insert___spec__3___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_NameSet_HasEmptyc;
 lean_object* l_Lean_NameMap_find___rarg___boxed(lean_object*, lean_object*);
-lean_object* l_Lean_Name_mkString___boxed(lean_object* x_1, lean_object* x_2) {
+lean_object* l_Lean_Name_str___boxed(lean_object*, lean_object*);
+lean_object* l_Lean_Name_str___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
@@ -151,7 +150,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-lean_object* l_Lean_Name_mkNumeral___boxed(lean_object* x_1, lean_object* x_2) {
+lean_object* l_Lean_Name_num___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
@@ -159,6 +158,14 @@ x_3 = lean_name_mk_numeral(x_1, x_2);
 return x_3;
 }
 }
+lean_object* l_Lean_Name_mkString(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
 lean_object* _init_l_Lean_Inhabited() {
 _start:
 {
@@ -167,7 +174,7 @@ x_1 = lean_box(0);
 return x_1;
 }
 }
-lean_object* l_Lean_mkStrName(lean_object* x_1, lean_object* x_2) {
+lean_object* l_Lean_mkNameStr(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
@@ -175,7 +182,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-lean_object* l_Lean_mkNumName(lean_object* x_1, lean_object* x_2) {
+lean_object* l_Lean_mkNameNum(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
@@ -183,7 +190,7 @@ x_3 = lean_name_mk_numeral(x_1, x_2);
 return x_3;
 }
 }
-lean_object* l_Lean_mkSimpleName(lean_object* x_1) {
+lean_object* l_Lean_mkNameSimple(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
@@ -196,7 +203,7 @@ lean_object* _init_l_Lean_stringToName___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_mkSimpleName), 1, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_mkNameSimple), 1, 0);
 return x_1;
 }
 }
@@ -9039,22 +9046,6 @@ x_4 = lean_box(x_3);
 return x_4;
 }
 }
-lean_object* l_Lean_mkNameStr(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; 
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-lean_object* l_Lean_mkNameNum(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; 
-x_3 = lean_name_mk_numeral(x_1, x_2);
-return x_3;
-}
-}
 lean_object* l_List_foldl___main___at_String_toName___spec__1(lean_object* x_1, lean_object* x_2) {
 _start:
 {
diff --git a/stage0/library/Init/Lean/NameGenerator.c b/stage0/library/Init/Lean/NameGenerator.c
index 35e240a83d..1de2df744f 100644
--- a/stage0/library/Init/Lean/NameGenerator.c
+++ b/stage0/library/Init/Lean/NameGenerator.c
@@ -13,15 +13,15 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* l_Lean_NameGenerator_mkChild(lean_object*);
 lean_object* l_Lean_NameGenerator_Inhabited___closed__1;
 lean_object* l_Lean_NameGenerator_next(lean_object*);
 lean_object* l_Lean_NameGenerator_Inhabited___closed__3;
-lean_object* l_Lean_NameGenerator_Inhabited___closed__2;
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
+lean_object* l_Lean_NameGenerator_Inhabited___closed__2;
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Lean_NameGenerator_curr(lean_object*);
-lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* l_Lean_NameGenerator_Inhabited;
 lean_object* _init_l_Lean_NameGenerator_Inhabited___closed__1() {
 _start:
diff --git a/stage0/library/Init/Lean/Options.c b/stage0/library/Init/Lean/Options.c
index 9a1ca6c83d..4cb7200bef 100644
--- a/stage0/library/Init/Lean/Options.c
+++ b/stage0/library/Init/Lean/Options.c
@@ -30,13 +30,13 @@ extern lean_object* l_Bool_HasRepr___closed__2;
 lean_object* l_Lean_setOptionFromString___closed__1;
 lean_object* l_RBNode_find___main___at_Lean_getOptionDecl___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_KVMap_setInt(lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Options_1__initOptionDeclsRef(lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
 lean_object* l_Lean_KVMap_setName(lean_object*, lean_object*, lean_object*);
 lean_object* l_RBNode_find___main___at_Lean_getOptionDecl___spec__1___boxed(lean_object*, lean_object*);
 extern lean_object* l_Char_HasRepr___closed__1;
 lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_registerOption(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_NameMap_contains___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_setOptionFromString___closed__4;
diff --git a/stage0/library/Init/Lean/Parser/Command.c b/stage0/library/Init/Lean/Parser/Command.c
index 7ca683bdcc..b0cdd1045f 100644
--- a/stage0/library/Init/Lean/Parser/Command.c
+++ b/stage0/library/Init/Lean/Parser/Command.c
@@ -481,6 +481,7 @@ lean_object* l_Lean_Parser_Command_protected___closed__3;
 lean_object* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__6;
 lean_object* l_Lean_Parser_Command_partial___closed__4;
 lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_mixfixKind___elambda__1___boxed(lean_object*);
 lean_object* l_Lean_Parser_Command_attribute___closed__3;
 lean_object* l_Lean_Parser_Command_partial___closed__1;
@@ -640,7 +641,6 @@ lean_object* l_Lean_Parser_Command_quotedSymbolPrec___closed__6;
 lean_object* l_Lean_Parser_Command_symbol___closed__4;
 lean_object* l_Lean_Parser_Command_private___elambda__1(lean_object*);
 lean_object* l_Lean_Parser_Command_init__quot___elambda__1___rarg(lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_example___closed__5;
 lean_object* l_Lean_Parser_Command_quotedSymbolPrec___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Command_inferMod___closed__1;
diff --git a/stage0/library/Init/Lean/Parser/Level.c b/stage0/library/Init/Lean/Parser/Level.c
index ed74ff0c67..0f83af1254 100644
--- a/stage0/library/Init/Lean/Parser/Level.c
+++ b/stage0/library/Init/Lean/Parser/Level.c
@@ -72,6 +72,7 @@ lean_object* l_Lean_Parser_Level_paren___elambda__1(lean_object*);
 lean_object* l_Lean_Parser_Level_paren___elambda__1___rarg___closed__8;
 lean_object* l_Lean_Parser_Level_paren___elambda__1___rarg___closed__11;
 lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_max___closed__4;
 lean_object* l_Lean_Parser_Level_paren___elambda__1___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_max___closed__1;
@@ -94,7 +95,6 @@ extern lean_object* l_Char_HasRepr___closed__1;
 lean_object* l_Lean_Parser_levelParserAttribute;
 lean_object* l_Lean_Parser_mkLevelParserAttribute___closed__2;
 lean_object* l_Lean_Parser_Level_paren___closed__7;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Level_num___elambda__1(lean_object*);
 lean_object* l_Lean_Parser_regBuiltinLevelParserAttr___closed__4;
diff --git a/stage0/library/Init/Lean/Parser/Module.c b/stage0/library/Init/Lean/Parser/Module.c
index 149a9dfd6d..a89bfeaf4e 100644
--- a/stage0/library/Init/Lean/Parser/Module.c
+++ b/stage0/library/Init/Lean/Parser/Module.c
@@ -65,6 +65,7 @@ lean_object* l_Lean_Parser_Module_header___closed__2;
 lean_object* l___private_Init_Lean_Parser_Module_3__consumeInput(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_testModuleParser___closed__1;
 lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Module_header___closed__1;
 lean_object* l_Lean_Parser_Module_import___closed__3;
 lean_object* l_Lean_Parser_Module_header___elambda__1___closed__1;
@@ -84,7 +85,6 @@ extern lean_object* l_Char_HasRepr___closed__1;
 lean_object* l_Lean_Parser_Module_import___elambda__1___closed__4;
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Module_importPath___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Module_import;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_testModuleParser___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Module_importPath___closed__4;
 lean_object* l_Lean_Parser_Module_importPath___closed__3;
diff --git a/stage0/library/Init/Lean/Parser/Parser.c b/stage0/library/Init/Lean/Parser/Parser.c
index 4bcbec9218..9f3bbe6118 100644
--- a/stage0/library/Init/Lean/Parser/Parser.c
+++ b/stage0/library/Init/Lean/Parser/Parser.c
@@ -343,6 +343,7 @@ uint8_t l_HashMapImp_contains___at_Lean_Parser_isValidSyntaxNodeKind___spec__1(l
 lean_object* l_Lean_Parser_trailingNode(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
 size_t lean_name_hash_usize(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_Lean_Parser_ParserState_next___boxed(lean_object*, lean_object*, lean_object*);
@@ -437,7 +438,6 @@ lean_object* l_Lean_Parser_whitespace___boxed(lean_object*, lean_object*);
 lean_object* l_List_append___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_fieldIdxFn___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_declareBuiltinParser___closed__2;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 uint8_t l___private_Init_Lean_Parser_Parser_4__isToken(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_decimalNumberFn___spec__2(lean_object*, lean_object*);
 lean_object* l_Lean_nameToExprAux___main(lean_object*);
diff --git a/stage0/library/Init/Lean/Parser/Term.c b/stage0/library/Init/Lean/Parser/Term.c
index 2528cf77c7..b5247dd736 100644
--- a/stage0/library/Init/Lean/Parser/Term.c
+++ b/stage0/library/Init/Lean/Parser/Term.c
@@ -681,6 +681,7 @@ lean_object* l_Lean_Parser_Term_nomatch___elambda__1___rarg___closed__1;
 lean_object* l___regBuiltinParser_Lean_Parser_Term_seqRight(lean_object*);
 lean_object* l_Lean_Parser_Term_sub___elambda__1___closed__3;
 lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_listLit___closed__7;
 lean_object* l_Lean_Parser_Term_doLet___closed__4;
 lean_object* l___regBuiltinParser_Lean_Parser_Term_suffices(lean_object*);
@@ -858,7 +859,6 @@ lean_object* l_Lean_Parser_Term_bracketedDoSeq___closed__3;
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letEqns___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinParser_Lean_Parser_Term_sorry(lean_object*);
 lean_object* l_Lean_Parser_Term_if___elambda__1___rarg___closed__4;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_explicit___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_uminus___closed__1;
 lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__15;
diff --git a/stage0/library/Init/Lean/Parser/Transform.c b/stage0/library/Init/Lean/Parser/Transform.c
index e2c2e871fe..19a7920a64 100644
--- a/stage0/library/Init/Lean/Parser/Transform.c
+++ b/stage0/library/Init/Lean/Parser/Transform.c
@@ -21,13 +21,13 @@ lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_declareLeadingBuiltinParser___closed__1;
 lean_object* l_Lean_Syntax_removeParen___closed__1;
 lean_object* l_Lean_Syntax_getTailInfo___main___rarg(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 uint8_t l_Lean_Syntax_isNone___rarg(lean_object*);
 lean_object* l_Lean_Syntax_getArg___rarg(lean_object*, lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
 extern lean_object* l_Option_HasRepr___rarg___closed__3;
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l_Lean_SourceInfo_truncateTrailing(lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_manyToSepBy___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Path.c b/stage0/library/Init/Lean/Path.c
index 3e6a6b5ac2..c3e92ea86b 100644
--- a/stage0/library/Init/Lean/Path.c
+++ b/stage0/library/Init/Lean/Path.c
@@ -52,6 +52,7 @@ lean_object* lean_io_getenv(lean_object*, lean_object*);
 extern lean_object* l_List_repr___rarg___closed__2;
 lean_object* l_Lean_getSearchPathFromEnv___closed__2;
 lean_object* l_Lean_findFile(lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* lean_io_file_exists(lean_object*, lean_object*);
 lean_object* l_Lean_realPathNormalized(lean_object*, lean_object*);
 lean_object* l_Lean_modNameToFileName___boxed(lean_object*);
@@ -70,7 +71,6 @@ lean_object* l_List_reprAux___main___at_Lean_findAtSearchPath___spec__3___boxed(
 lean_object* l_System_FilePath_dirName(lean_object*);
 lean_object* l_Lean_getBuiltinSearchPath___closed__1;
 lean_object* l_List_append___rarg(lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_List_foldl___main___at_Lean_moduleNameOfFileName___spec__1(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Lean_findLeanFile___closed__2;
diff --git a/stage0/library/Init/Lean/ProjFns.c b/stage0/library/Init/Lean/ProjFns.c
index 0b7f2d80c6..5d1f62ac85 100644
--- a/stage0/library/Init/Lean/ProjFns.c
+++ b/stage0/library/Init/Lean/ProjFns.c
@@ -46,6 +46,7 @@ lean_object* lean_io_initializing(lean_object*);
 lean_object* lean_mk_empty_array_with_capacity(lean_object*);
 lean_object* l_Lean_projectionFnInfoExt___elambda__3___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_projectionFnInfoExt___elambda__4(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_Lean_projectionFnInfoExt___elambda__4___rarg(lean_object*);
 lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_mkProjectionFnInfoExtension___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -61,7 +62,6 @@ lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_obje
 uint8_t l_Lean_Environment_isProjectionFn(lean_object*, lean_object*);
 uint8_t l_Array_anyRangeMAux___main___at_Lean_mkProjectionFnInfoExtension___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_mkProjectionFnInfoExtension___spec__2___closed__1;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_projectionFnInfoExt___closed__1;
 lean_object* lean_nat_add(lean_object*, lean_object*);
 extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;
diff --git a/stage0/library/Init/Lean/ReducibilityAttrs.c b/stage0/library/Init/Lean/ReducibilityAttrs.c
index 0dc8f53680..c999512527 100644
--- a/stage0/library/Init/Lean/ReducibilityAttrs.c
+++ b/stage0/library/Init/Lean/ReducibilityAttrs.c
@@ -59,6 +59,7 @@ extern lean_object* l_Lean_EnumAttributes_Inhabited___closed__1;
 lean_object* l_Lean_mkReducibilityAttrs___closed__8;
 lean_object* l_Lean_mkReducibilityAttrs___lambda__1(lean_object*, lean_object*, uint8_t);
 lean_object* l_List_forM___main___at_Lean_registerEnumAttributes___spec__11(lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_mkReducibilityAttrs___closed__3;
@@ -71,7 +72,6 @@ lean_object* l_Lean_mkReducibilityAttrs___closed__11;
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l_Lean_mkReducibilityAttrs___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_RBNode_fold___main___at_Lean_mkReducibilityAttrs___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_registerEnumAttributes___at_Lean_mkReducibilityAttrs___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Scopes.c b/stage0/library/Init/Lean/Scopes.c
index a84e51ac2f..43e7ceccd9 100644
--- a/stage0/library/Init/Lean/Scopes.c
+++ b/stage0/library/Init/Lean/Scopes.c
@@ -55,6 +55,7 @@ lean_object* l_Lean_Environment_inSection___boxed(lean_object*);
 lean_object* l_RBNode_insert___at_Lean_NameSet_insert___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_regScopeManagerExtension___lambda__2___boxed(lean_object*);
 lean_object* l_Lean_regScopeManagerExtension(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Environment_getNamespaceSet(lean_object*);
 extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_regScopeManagerExtension___spec__1___boxed(lean_object*, lean_object*);
@@ -63,7 +64,6 @@ lean_object* lean_string_append(lean_object*, lean_object*);
 lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_regScopeManagerExtension___spec__5(lean_object*, lean_object*);
 lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;
 uint8_t lean_is_namespace(lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/Syntax.c b/stage0/library/Init/Lean/Syntax.c
index fe60563c2a..a1068aa440 100644
--- a/stage0/library/Init/Lean/Syntax.c
+++ b/stage0/library/Init/Lean/Syntax.c
@@ -120,6 +120,7 @@ lean_object* l_Lean_Syntax_getIdAt(lean_object*);
 lean_object* l_Lean_mkAtomFrom___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_mreplace___main___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_updateTrailing___rarg(lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_mreplace___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_mkStxNumLit(lean_object*, lean_object*);
 lean_object* l_Lean_numLitKind___closed__2;
@@ -170,7 +171,6 @@ lean_object* l_Lean_unreachIsNodeAtom(lean_object*, lean_object*, lean_object*,
 lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_findMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1(lean_object*);
 lean_object* l___private_Init_Lean_Syntax_5__decodeBinLitAux___boxed(lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_mrewriteBottomUp___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getKind(lean_object*);
 lean_object* l___private_Init_Lean_Syntax_5__decodeBinLitAux___main___boxed(lean_object*, lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/ToExpr.c b/stage0/library/Init/Lean/ToExpr.c
index 9800c63237..e2dcaba210 100644
--- a/stage0/library/Init/Lean/ToExpr.c
+++ b/stage0/library/Init/Lean/ToExpr.c
@@ -18,14 +18,13 @@ lean_object* l_Lean_mkStrLit(lean_object*);
 lean_object* l_Lean_nameToExprAux___main___closed__3;
 lean_object* l_Lean_nameToExprAux___main___closed__1;
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_nameToExprAux___main___closed__7;
 lean_object* l_Lean_nameToExprAux___main___closed__8;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_nameToExprAux___main(lean_object*);
 extern lean_object* l_liftRefl___closed__1;
 lean_object* l_Lean_nameToExprAux___main___closed__6;
 lean_object* l_Lean_nameToExprAux(lean_object*);
-lean_object* l_Lean_nameToExprAux___main___closed__9;
 lean_object* l_Lean_mkNatLit(lean_object*);
 lean_object* l_Lean_mkCAppB(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_strToExpr___closed__1;
@@ -114,45 +113,35 @@ return x_3;
 lean_object* _init_l_Lean_nameToExprAux___main___closed__5() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_nameToExprAux___main___closed__4;
-x_2 = l_Lean_nameToExprAux___main___closed__2;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
+lean_object* x_1; 
+x_1 = lean_mk_string("mkNameStr");
+return x_1;
 }
 }
 lean_object* _init_l_Lean_nameToExprAux___main___closed__6() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("mkString");
-return x_1;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_nameToExprAux___main___closed__4;
+x_2 = l_Lean_nameToExprAux___main___closed__5;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
 }
 }
 lean_object* _init_l_Lean_nameToExprAux___main___closed__7() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_nameToExprAux___main___closed__5;
-x_2 = l_Lean_nameToExprAux___main___closed__6;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
+lean_object* x_1; 
+x_1 = lean_mk_string("mkNameNum");
+return x_1;
 }
 }
 lean_object* _init_l_Lean_nameToExprAux___main___closed__8() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("mkNumeral");
-return x_1;
-}
-}
-lean_object* _init_l_Lean_nameToExprAux___main___closed__9() {
-_start:
-{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_nameToExprAux___main___closed__5;
-x_2 = l_Lean_nameToExprAux___main___closed__8;
+x_1 = l_Lean_nameToExprAux___main___closed__4;
+x_2 = l_Lean_nameToExprAux___main___closed__7;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@@ -184,7 +173,7 @@ lean_inc(x_11);
 lean_dec(x_1);
 x_12 = l_Lean_nameToExprAux___main(x_10);
 x_13 = l_Lean_mkStrLit(x_11);
-x_14 = l_Lean_nameToExprAux___main___closed__7;
+x_14 = l_Lean_nameToExprAux___main___closed__6;
 x_15 = l_Lean_mkCAppB(x_14, x_12, x_13);
 return x_15;
 }
@@ -198,7 +187,7 @@ lean_inc(x_17);
 lean_dec(x_1);
 x_18 = l_Lean_nameToExprAux___main(x_16);
 x_19 = l_Lean_mkNatLit(x_17);
-x_20 = l_Lean_nameToExprAux___main___closed__9;
+x_20 = l_Lean_nameToExprAux___main___closed__8;
 x_21 = l_Lean_mkCAppB(x_20, x_18, x_19);
 return x_21;
 }
@@ -264,8 +253,6 @@ l_Lean_nameToExprAux___main___closed__7 = _init_l_Lean_nameToExprAux___main___cl
 lean_mark_persistent(l_Lean_nameToExprAux___main___closed__7);
 l_Lean_nameToExprAux___main___closed__8 = _init_l_Lean_nameToExprAux___main___closed__8();
 lean_mark_persistent(l_Lean_nameToExprAux___main___closed__8);
-l_Lean_nameToExprAux___main___closed__9 = _init_l_Lean_nameToExprAux___main___closed__9();
-lean_mark_persistent(l_Lean_nameToExprAux___main___closed__9);
 l_Lean_nameToExpr___closed__1 = _init_l_Lean_nameToExpr___closed__1();
 lean_mark_persistent(l_Lean_nameToExpr___closed__1);
 l_Lean_nameToExpr = _init_l_Lean_nameToExpr();
diff --git a/stage0/library/Init/Lean/Trace.c b/stage0/library/Init/Lean/Trace.c
index 6d0de0ad59..16a3df7f6f 100644
--- a/stage0/library/Init/Lean/Trace.c
+++ b/stage0/library/Init/Lean/Trace.c
@@ -48,6 +48,7 @@ lean_object* l___private_Init_Lean_Trace_5__checkTraceOption___rarg___lambda__1_
 lean_object* l_Lean_MonadTracerAdapter_traceCtx___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_TraceState_HasToString;
 lean_object* l_Lean_SimpleMonadTracerAdapter_getTraces___rarg(lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_SimpleMonadTracerAdapter_isTracingEnabledFor___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_monadTracerAdapter___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_SimpleMonadTracerAdapter_getTraces(lean_object*);
@@ -63,7 +64,6 @@ uint8_t l___private_Init_Lean_Trace_4__checkTraceOptionAux(lean_object*, lean_ob
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Trace_5__checkTraceOption___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_SimpleMonadTracerAdapter_enableTracing___rarg___boxed(lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Lean_MonadTracerAdapter_trace___boxed(lean_object*);
 lean_object* l_Lean_SimpleMonadTracerAdapter_modifyTraces___rarg(lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/TypeClass/Context.c b/stage0/library/Init/Lean/TypeClass/Context.c
index 45d756927b..d6a179b95b 100644
--- a/stage0/library/Init/Lean/TypeClass/Context.c
+++ b/stage0/library/Init/Lean/TypeClass/Context.c
@@ -20,6 +20,7 @@ uint8_t l_Lean_TypeClass_Context_eHasETmpMVar(lean_object*);
 lean_object* l_Lean_Expr_bindingBody_x21(lean_object*);
 lean_object* l_Lean_TypeClass_Context_internalize___lambda__2(lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_Context_eHasTmpMVar___closed__1;
+lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 uint8_t l_Lean_Name_beq___main(lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_Context_internalize___closed__4;
 lean_object* l_Lean_TypeClass_Context_eMetaNormalizeCore___rarg(lean_object*, lean_object*, lean_object*);
@@ -104,6 +105,7 @@ uint8_t l_Lean_TypeClass_Context_eFind___main(lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_Context_eIsMeta___boxed(lean_object*);
 lean_object* l_Lean_TypeClass_Context__u03b1Norm___lambda__2(lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_Context_uIsMeta___boxed(lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 uint8_t lean_expr_eqv(lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_Context_uInstantiate___main___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_Context_eUnify___main___closed__4;
@@ -129,7 +131,6 @@ lean_object* lean_expr_update_const(lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_Context_eInstantiate(lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_Context_eMetaIdx___boxed(lean_object*);
 lean_object* l_Lean_TypeClass_Context_eAssignIdx___boxed(lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 uint8_t l_List_foldr___main___at_Lean_TypeClass_Context_eHasTmpMVar___spec__1(uint8_t, lean_object*);
 extern lean_object* l___private_Init_Lean_MetavarContext_5__instantiateDelayedAux___main___closed__1;
 lean_object* l_PersistentArray_getAux___main___at_Lean_TypeClass_Context_eInferIdx___spec__2___boxed(lean_object*, lean_object*, lean_object*);
@@ -168,7 +169,6 @@ lean_object* l_Lean_TypeClass_Context_uAssignIdx(lean_object*, lean_object*, lea
 lean_object* l_Lean_TypeClass_Context_slowWhnfApp___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_RBNode_insert___at_Lean_TypeClass_Context__u03b1Norm___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentArray_getAux___main___at_Lean_TypeClass_Context_eLookupIdx___spec__2___boxed(lean_object*, lean_object*, lean_object*);
-lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_Context_uInstantiate___main(lean_object*, lean_object*);
 uint8_t l_Lean_TypeClass_Context_uOccursIn(lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_Context_eInfer___closed__2;
diff --git a/stage0/library/Init/Lean/TypeClass/Synth.c b/stage0/library/Init/Lean/TypeClass/Synth.c
index bd088691e4..bafde6e814 100644
--- a/stage0/library/Init/Lean/TypeClass/Synth.c
+++ b/stage0/library/Init/Lean/TypeClass/Synth.c
@@ -15,6 +15,7 @@ extern "C" {
 #endif
 lean_object* l_PersistentHashMap_insertAux___main___at_Lean_TypeClass_newSubgoal___spec__3(lean_object*, size_t, size_t, lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_introduceLocals(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 size_t l_USize_mul(size_t, size_t);
 lean_object* l_Lean_TypeClass_synth___closed__2;
 extern lean_object* l_Array_empty___closed__1;
@@ -85,6 +86,7 @@ lean_object* l_PersistentHashMap_insertAux___main___at_Lean_TypeClass_newSubgoal
 lean_object* l_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_Node_Inhabited___closed__1;
 extern lean_object* l_Lean_TypeClass_Context_Inhabited;
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_constNameToTypedExpr(lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_TypeClass_newAnswer___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_expr_eqv(lean_object*, lean_object*);
@@ -110,7 +112,6 @@ uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l_Lean_mkFVar(lean_object*);
 lean_object* l_Lean_TypeClass_collectEReplacements(lean_object*);
 lean_object* l_List_append___rarg(lean_object*, lean_object*);
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_collectEReplacements___main___closed__2;
 lean_object* l_Lean_TypeClass_ConsumerNode_Inhabited___closed__1;
 lean_object* lean_nat_add(lean_object*, lean_object*);
@@ -152,7 +153,6 @@ lean_object* lean_array_pop(lean_object*);
 lean_object* lean_instantiate_type_lparams(lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_newSubgoal___closed__3;
 lean_object* l_Lean_TypeClass_preprocessForOutParams(lean_object*, lean_object*);
-lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 lean_object* lean_environment_find(lean_object*, lean_object*);
 lean_object* l_Lean_TypeClass_collectEReplacements___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_is_class(lean_object*, lean_object*);
diff --git a/stage0/library/Init/Lean/WHNF.c b/stage0/library/Init/Lean/WHNF.c
index 7d42679317..8d92589885 100644
--- a/stage0/library/Init/Lean/WHNF.c
+++ b/stage0/library/Init/Lean/WHNF.c
@@ -89,6 +89,7 @@ lean_object* l_Lean_whnfCore___boxed(lean_object*);
 lean_object* l___private_Init_Lean_WHNF_3__toCtorIfLit___closed__1;
 lean_object* l_Lean_mkSmartUnfoldingNameFor(lean_object*);
 lean_object* l_Lean_reduceQuotRec___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 uint8_t lean_expr_eqv(lean_object*, lean_object*);
 lean_object* l_Lean_whnfCore___main___rarg___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_ConstantInfo_hasValue(lean_object*);
@@ -107,7 +108,6 @@ lean_object* l_Lean_reduceRec___rarg___lambda__3(lean_object*, lean_object*, lea
 lean_object* l___private_Init_Lean_WHNF_3__toCtorIfLit___boxed(lean_object*);
 lean_object* l_Lean_whnfMain___boxed(lean_object*);
 lean_object* l___private_Init_Lean_WHNF_3__toCtorIfLit___closed__4;
-lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_unfoldDefinitionAux___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
 lean_object* lean_instantiate_value_lparams(lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
diff --git a/stage0/src/frontends/lean/parser.cpp b/stage0/src/frontends/lean/parser.cpp
index 33b5d97ae9..58954ba076 100644
--- a/stage0/src/frontends/lean/parser.cpp
+++ b/stage0/src/frontends/lean/parser.cpp
@@ -1527,7 +1527,7 @@ struct to_pattern_fn {
         buffer<expr> args;
         get_app_args(e, args);
         args[0] = fix_quoted_name(args[0]);
-        return mk_app(mk_constant(get_lean_name_mk_string_name()), args);
+        return mk_app(mk_constant(get_lean_name_str_name()), args);
     }
 
     expr fix_quoted_names(expr const & e) {
diff --git a/stage0/src/library/constants.cpp b/stage0/src/library/constants.cpp
index a526c40d2c..5b508477bd 100644
--- a/stage0/src/library/constants.cpp
+++ b/stage0/src/library/constants.cpp
@@ -116,8 +116,8 @@ name const * g_monad = nullptr;
 name const * g_monad_fail = nullptr;
 name const * g_lean_name = nullptr;
 name const * g_lean_name_anonymous = nullptr;
-name const * g_lean_name_mk_numeral = nullptr;
-name const * g_lean_name_mk_string = nullptr;
+name const * g_lean_name_num = nullptr;
+name const * g_lean_name_str = nullptr;
 name const * g_lean_mk_name_num = nullptr;
 name const * g_lean_mk_name_str = nullptr;
 name const * g_lean_parser_leading_node = nullptr;
@@ -305,8 +305,8 @@ void initialize_constants() {
     g_monad_fail = new name{"MonadFail"};
     g_lean_name = new name{"Lean", "Name"};
     g_lean_name_anonymous = new name{"Lean", "Name", "anonymous"};
-    g_lean_name_mk_numeral = new name{"Lean", "Name", "mkNumeral"};
-    g_lean_name_mk_string = new name{"Lean", "Name", "mkString"};
+    g_lean_name_num = new name{"Lean", "Name", "num"};
+    g_lean_name_str = new name{"Lean", "Name", "str"};
     g_lean_mk_name_num = new name{"Lean", "mkNameNum"};
     g_lean_mk_name_str = new name{"Lean", "mkNameStr"};
     g_lean_parser_leading_node = new name{"Lean", "Parser", "leadingNode"};
@@ -495,8 +495,8 @@ void finalize_constants() {
     delete g_monad_fail;
     delete g_lean_name;
     delete g_lean_name_anonymous;
-    delete g_lean_name_mk_numeral;
-    delete g_lean_name_mk_string;
+    delete g_lean_name_num;
+    delete g_lean_name_str;
     delete g_lean_mk_name_num;
     delete g_lean_mk_name_str;
     delete g_lean_parser_leading_node;
@@ -684,8 +684,8 @@ name const & get_monad_name() { return *g_monad; }
 name const & get_monad_fail_name() { return *g_monad_fail; }
 name const & get_lean_name_name() { return *g_lean_name; }
 name const & get_lean_name_anonymous_name() { return *g_lean_name_anonymous; }
-name const & get_lean_name_mk_numeral_name() { return *g_lean_name_mk_numeral; }
-name const & get_lean_name_mk_string_name() { return *g_lean_name_mk_string; }
+name const & get_lean_name_num_name() { return *g_lean_name_num; }
+name const & get_lean_name_str_name() { return *g_lean_name_str; }
 name const & get_lean_mk_name_num_name() { return *g_lean_mk_name_num; }
 name const & get_lean_mk_name_str_name() { return *g_lean_mk_name_str; }
 name const & get_lean_parser_leading_node_name() { return *g_lean_parser_leading_node; }
diff --git a/stage0/src/library/constants.h b/stage0/src/library/constants.h
index 73d5934b65..329194664d 100644
--- a/stage0/src/library/constants.h
+++ b/stage0/src/library/constants.h
@@ -118,8 +118,8 @@ name const & get_monad_name();
 name const & get_monad_fail_name();
 name const & get_lean_name_name();
 name const & get_lean_name_anonymous_name();
-name const & get_lean_name_mk_numeral_name();
-name const & get_lean_name_mk_string_name();
+name const & get_lean_name_num_name();
+name const & get_lean_name_str_name();
 name const & get_lean_mk_name_num_name();
 name const & get_lean_mk_name_str_name();
 name const & get_lean_parser_leading_node_name();
diff --git a/stage0/src/library/constants.txt b/stage0/src/library/constants.txt
index 66f7a6e47f..f51defdb79 100644
--- a/stage0/src/library/constants.txt
+++ b/stage0/src/library/constants.txt
@@ -111,8 +111,8 @@ Monad
 MonadFail
 Lean.Name
 Lean.Name.anonymous
-Lean.Name.mkNumeral
-Lean.Name.mkString
+Lean.Name.num
+Lean.Name.str
 Lean.mkNameNum
 Lean.mkNameStr
 Lean.Parser.leadingNode
diff --git a/stage0/src/library/util.cpp b/stage0/src/library/util.cpp
index 07a60fe78b..cd64296fe4 100644
--- a/stage0/src/library/util.cpp
+++ b/stage0/src/library/util.cpp
@@ -1009,12 +1009,12 @@ optional<name> is_unsafe_rec_name(name const & n) {
 optional<name> name_lit_to_name(expr const & name_lit) {
     if (is_constant(name_lit, get_lean_name_anonymous_name()))
         return optional<name>(name());
-    if (is_app_of(name_lit, get_lean_name_mk_string_name(), 2)) {
+    if (is_app_of(name_lit, get_lean_name_str_name(), 2)) {
         if (auto p   = name_lit_to_name(app_arg(app_fn(name_lit))))
         if (auto str = to_string(app_arg(name_lit)))
             return optional<name>(name(*p, str->c_str()));
     }
-    if (is_app_of(name_lit, get_lean_name_mk_numeral_name(), 2)) {
+    if (is_app_of(name_lit, get_lean_name_num_name(), 2)) {
         if (auto p = name_lit_to_name(app_arg(app_fn(name_lit))))
         if (auto n = to_num(app_arg(name_lit)))
             return optional<name>(name(*p, n->get_unsigned_int()));