diff --git a/stage0/src/Lean/Elab/BuiltinNotation.lean b/stage0/src/Lean/Elab/BuiltinNotation.lean
index b18be09973..4ecebdd9e5 100644
--- a/stage0/src/Lean/Elab/BuiltinNotation.lean
+++ b/stage0/src/Lean/Elab/BuiltinNotation.lean
@@ -364,4 +364,13 @@ private def elabCDot (stx : Syntax) (expectedType? : Option Expr) : TermElabM Ex
        mkEqNDRec (← mkMotive expectedAbst) h heq
   | _ => throwUnsupportedSyntax
 
+@[builtinTermElab stateRefT] def elabStateRefT : TermElab := fun stx _ => do
+  let σ ← elabType stx[1]
+  let m ← elabTerm stx[2] (← mkArrow (mkSort levelOne) (mkSort levelOne))
+  let ω ← mkFreshExprMVar (mkSort levelOne)
+  let stWorld ← mkAppM `STWorld #[ω, m]
+  mkInstMVar stWorld
+  mkAppM `StateRefT' #[ω, σ, m]
+
+
 end Lean.Elab.Term
diff --git a/stage0/src/Lean/Parser/Term.lean b/stage0/src/Lean/Parser/Term.lean
index 42aa7bbc5b..2050bdd6e6 100644
--- a/stage0/src/Lean/Parser/Term.lean
+++ b/stage0/src/Lean/Parser/Term.lean
@@ -259,8 +259,8 @@ def isIdent (stx : Syntax) : Bool :=
 @[builtinTermParser] def dbgTrace    := parser!:leadPrec withPosition ("dbgTrace! " >> ((interpolatedStr termParser) <|> termParser)) >> optSemicolon termParser
 @[builtinTermParser] def assert      := parser!:leadPrec withPosition ("assert! " >> termParser) >> optSemicolon termParser
 
--- Macro for avoiding exponentially big terms when using due to `STWorld`
-@[builtinTermParser] def stateRefT   := parser! "StateRefTNew" >> termParser maxPrec >> termParser maxPrec
+-- Macro for avoiding exponentially big terms when using `STWorld`
+@[builtinTermParser] def stateRefT   := parser! "StateRefT" >> termParser maxPrec >> termParser maxPrec
 
 end Term
 
diff --git a/stage0/stdlib/Lean/Elab/BuiltinNotation.c b/stage0/stdlib/Lean/Elab/BuiltinNotation.c
index cdd52c2279..030275c0af 100644
--- a/stage0/stdlib/Lean/Elab/BuiltinNotation.c
+++ b/stage0/stdlib/Lean/Elab/BuiltinNotation.c
@@ -53,6 +53,7 @@ extern lean_object* l___kind_term____x40_Init_Data_ToString_Macro___hyg_2____clo
 lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_getRefPos___at_Lean_Elab_Term_elabPanic___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_elabLetDeclCore___spec__1___rarg(lean_object*);
+lean_object* l_Lean_mkSort(lean_object*);
 lean_object* l_Lean_Elab_Term_expandPrefixOp___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_953____closed__7;
 lean_object* l_Lean_Elab_Term_expandModN___closed__3;
@@ -356,6 +357,7 @@ lean_object* l_Lean_Elab_Term_expandDiv___closed__1;
 extern lean_object* l_Lean_Meta_mkDecide___rarg___closed__1;
 lean_object* l_Lean_Elab_Term_expandPow(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabNativeRefl___lambda__1___closed__5;
+lean_object* l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__1;
 lean_object* l___regBuiltin_Lean_Elab_Term_expandBAnd___closed__1;
 lean_object* l___regBuiltin_Lean_Elab_Term_expandProd(lean_object*);
 lean_object* l_Lean_Elab_Term_expandAndM(lean_object*, lean_object*, lean_object*);
@@ -374,6 +376,7 @@ lean_object* l_Lean_Elab_Term_expandUnreachable(lean_object*, lean_object*);
 extern lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__2___closed__10;
 lean_object* l_Lean_Elab_Term_ExpandFComp___closed__4;
 lean_object* l_Lean_Elab_Term_expandBAnd(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_mkInstMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_expandEmptyC___closed__1;
 uint8_t l_Lean_Expr_hasExprMVar(lean_object*);
 lean_object* l_Lean_Meta_mkEqSymm___at_Lean_Elab_Term_elabSubst___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -448,6 +451,7 @@ lean_object* lean_st_mk_ref(lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_expandGT(lean_object*);
 lean_object* l_Lean_Elab_Term_expandSub___closed__1;
 lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux_match__1(lean_object*);
+lean_object* l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__2;
 lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_expandAnd___closed__2;
 lean_object* l___regBuiltin_Lean_Elab_Term_elabParen___closed__1;
@@ -490,6 +494,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_expandUMinus(lean_object*);
 lean_object* l_Lean_Elab_Term_expandBNe___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_expandOrM(lean_object*);
 lean_object* l_Lean_Elab_Term_elabNativeRefl___lambda__1___closed__9;
+lean_object* l_Lean_Meta_mkArrow___at_Lean_Elab_Term_elabStateRefT___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Literal_type___closed__2;
 extern lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_953____closed__19;
 extern lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__1___closed__2;
@@ -509,6 +514,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_expandAnd___closed__3;
 lean_object* l___regBuiltin_Lean_Elab_Term_elabDecide___closed__2;
 uint8_t l_Lean_Expr_isConstOf(lean_object*, lean_object*);
 extern lean_object* l_Lean_Meta_mkLt___rarg___closed__4;
+lean_object* l_Lean_Elab_Term_elabStateRefT___closed__1;
 lean_object* l___regBuiltin_Lean_Elab_Term_elabPanic___closed__2;
 lean_object* l_Lean_Elab_Term_expandAssert___closed__13;
 lean_object* l_Lean_Elab_Term_expandMod___closed__3;
@@ -561,11 +567,13 @@ extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_299____clos
 lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabClosedTerm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_expandAssert___closed__6;
 lean_object* l_Lean_Elab_Term_expandLE___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_elabStateRefT___closed__2;
 lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_mkNativeReflAuxDecl___closed__1;
 lean_object* l_Lean_Elab_Term_expandShow___closed__6;
 lean_object* l_Lean_Elab_Term_expandBAnd___closed__1;
 lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_mkNativeReflAuxDecl___closed__2;
+lean_object* l_Lean_Elab_Term_elabStateRefT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_expandGE(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_elabDecide___closed__1;
 lean_object* l_Lean_Elab_Term_expandMul___boxed(lean_object*, lean_object*, lean_object*);
@@ -585,6 +593,7 @@ lean_object* l_Lean_Elab_Term_ExpandFComp___closed__1;
 lean_object* l___regBuiltin_Lean_Elab_Term_expandIff___closed__3;
 lean_object* l_Lean_Elab_Term_expandModN___closed__2;
 lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__25;
+lean_object* l_Lean_Elab_Term_elabStateRefT___closed__5;
 lean_object* l_Lean_Elab_Term_expandSubtype___closed__3;
 lean_object* l_Lean_Elab_Term_expandEq___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_expandModN___closed__3;
@@ -616,6 +625,7 @@ lean_object* l_Lean_Elab_Term_expandHave___closed__7;
 lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*);
 lean_object* lean_environment_main_module(lean_object*);
 extern lean_object* l___private_Init_LeanInit_0__Lean_quoteList___rarg___closed__7;
+lean_object* l_Lean_Elab_Term_elabStateRefT___closed__6;
 lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__5;
 lean_object* l_Lean_Elab_Term_elabSubst_match__3___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__28;
@@ -704,6 +714,7 @@ lean_object* l_Lean_Elab_Term_elabSubst___lambda__6(lean_object*, lean_object*,
 uint8_t l_Lean_Expr_isFVar(lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_expandEq(lean_object*);
 lean_object* l_Lean_Elab_Term_expandHave___closed__5;
+lean_object* l_Lean_mkForall(lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabParserMacro___closed__1;
 lean_object* l_Lean_Elab_Term_expandNe___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -724,6 +735,7 @@ lean_object* l_Lean_Elab_Term_expandseqLeft___closed__4;
 lean_object* l_Lean_Elab_Term_expandUnreachable___rarg___closed__9;
 lean_object* l___regBuiltin_Lean_Elab_Term_expandDollar(lean_object*);
 extern lean_object* l_Lean_Meta_mkSorry___rarg___lambda__1___closed__2;
+lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_expandAssert___closed__19;
 lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__9;
 lean_object* l_Lean_Elab_getRefPos___at_Lean_Elab_Term_elabPanic___spec__2___rarg(lean_object*, lean_object*, lean_object*);
@@ -776,6 +788,7 @@ extern lean_object* l_Lean_Elab_Term_elabLetDeclCore___closed__9;
 lean_object* l___regBuiltin_Lean_Elab_Term_expandMul___closed__1;
 lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__8;
 lean_object* l_Lean_Elab_Term_elabPanic___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_mkAppM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_isMonad_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_expandseqRight___closed__4;
 lean_object* l_Lean_Elab_Term_expandseqLeft___closed__1;
 lean_object* l_Lean_Elab_Term_expandseq(lean_object*, lean_object*, lean_object*);
@@ -788,7 +801,9 @@ lean_object* l___regBuiltin_Lean_Elab_Term_elabParserMacro___closed__1;
 lean_object* l_Lean_Elab_Term_mkPairs(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__5;
 lean_object* l_Lean_Elab_Term_expandSorry___rarg___closed__4;
+lean_object* l_Lean_Elab_Term_elabStateRefT___closed__3;
 lean_object* l_Lean_Elab_Term_expandInfix___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_elabStateRefT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_expandseqLeft___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkStxLit(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_expandOrElse(lean_object*);
@@ -822,6 +837,7 @@ lean_object* l_Lean_Elab_Term_expandMap___boxed(lean_object*, lean_object*, lean
 lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__13;
 lean_object* l_Lean_Elab_Term_expandMap___closed__1;
 lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__7;
+lean_object* l_Lean_Meta_mkArrow___at_Lean_Elab_Term_elabStateRefT___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_expandBEq(lean_object*);
 lean_object* l_Lean_Elab_Term_expandMapRev___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_expandAssert___closed__9;
@@ -849,6 +865,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_expandLT___closed__1;
 lean_object* l_Lean_Elab_Term_expandAssert___closed__8;
 lean_object* l_Lean_Elab_Term_expandUnreachable___rarg___closed__5;
 lean_object* l_Lean_Elab_Term_expandHave___closed__6;
+extern lean_object* l_Lean_levelOne;
 extern lean_object* l_myMacro____x40_Init_Data_ToString_Macro___hyg_39____closed__8;
 lean_object* l_Lean_Elab_Term_expandMap(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_expandGE___closed__3;
@@ -885,6 +902,7 @@ lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_getPropToDe
 lean_object* l_Lean_Meta_mkEqRefl___at_Lean_Elab_Term_elabNativeRefl___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_expandAnd___closed__2;
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
+lean_object* l___regBuiltin_Lean_Elab_Term_elabStateRefT(lean_object*);
 lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux___closed__4;
 lean_object* l_Lean_Elab_Term_expandAdd___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_expandShow___closed__14;
@@ -893,6 +911,8 @@ lean_object* l_Lean_Elab_Term_expandGT___closed__2;
 lean_object* l_Lean_Elab_Term_expandAssert___closed__1;
 lean_object* l_Lean_Elab_Term_elabSubst_match__2___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_expandOrElse(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_elabStateRefT___closed__4;
+extern lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoe___closed__3;
 lean_object* l_Lean_Elab_Term_expandUnreachable___rarg___closed__8;
 lean_object* l___regBuiltin_Lean_Elab_Term_expandseq(lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_elabAnonymousCtor___closed__1;
@@ -931,6 +951,7 @@ uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 extern lean_object* l_Lean_Meta_mkArrow___rarg___closed__2;
 lean_object* l_Lean_Elab_Term_expandAndThen(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_expandAssert___closed__4;
+lean_object* l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__3;
 lean_object* l_Lean_Elab_Term_elabSubst___closed__1;
 static lean_object* _init_l_Lean_Elab_Term_expandDollar___closed__1() {
 _start:
@@ -15852,6 +15873,379 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
+lean_object* l_Lean_Meta_mkArrow___at_Lean_Elab_Term_elabStateRefT___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+_start:
+{
+lean_object* x_10; lean_object* x_11; uint8_t x_12; 
+x_10 = l_Lean_Meta_mkArrow___rarg___closed__2;
+x_11 = l___private_Lean_CoreM_0__Lean_Core_mkFreshNameImp(x_10, x_7, x_8, x_9);
+x_12 = !lean_is_exclusive(x_11);
+if (x_12 == 0)
+{
+lean_object* x_13; uint8_t x_14; lean_object* x_15; 
+x_13 = lean_ctor_get(x_11, 0);
+x_14 = 0;
+x_15 = l_Lean_mkForall(x_13, x_14, x_1, x_2);
+lean_ctor_set(x_11, 0, x_15);
+return x_11;
+}
+else
+{
+lean_object* x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19; lean_object* x_20; 
+x_16 = lean_ctor_get(x_11, 0);
+x_17 = lean_ctor_get(x_11, 1);
+lean_inc(x_17);
+lean_inc(x_16);
+lean_dec(x_11);
+x_18 = 0;
+x_19 = l_Lean_mkForall(x_16, x_18, x_1, x_2);
+x_20 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_20, 0, x_19);
+lean_ctor_set(x_20, 1, x_17);
+return x_20;
+}
+}
+}
+static lean_object* _init_l_Lean_Elab_Term_elabStateRefT___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_levelOne;
+x_2 = l_Lean_mkSort(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_Elab_Term_elabStateRefT___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Elab_Term_elabStateRefT___closed__1;
+x_2 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_Elab_Term_elabStateRefT___closed__3() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("STWorld");
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_Elab_Term_elabStateRefT___closed__4() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Elab_Term_elabStateRefT___closed__3;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean_Elab_Term_elabStateRefT___closed__5() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("StateRefT'");
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_Elab_Term_elabStateRefT___closed__6() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Elab_Term_elabStateRefT___closed__5;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* l_Lean_Elab_Term_elabStateRefT(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+_start:
+{
+lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+x_10 = lean_unsigned_to_nat(1u);
+x_11 = l_Lean_Syntax_getArg(x_1, x_10);
+lean_inc(x_8);
+lean_inc(x_7);
+lean_inc(x_6);
+lean_inc(x_5);
+lean_inc(x_4);
+lean_inc(x_3);
+x_12 = l_Lean_Elab_Term_elabType(x_11, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
+if (lean_obj_tag(x_12) == 0)
+{
+lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23; 
+x_13 = lean_ctor_get(x_12, 0);
+lean_inc(x_13);
+x_14 = lean_ctor_get(x_12, 1);
+lean_inc(x_14);
+lean_dec(x_12);
+x_15 = l_Lean_Elab_Term_elabStateRefT___closed__1;
+x_16 = l_Lean_Meta_mkArrow___at_Lean_Elab_Term_elabStateRefT___spec__1(x_15, x_15, x_3, x_4, x_5, x_6, x_7, x_8, x_14);
+x_17 = lean_ctor_get(x_16, 0);
+lean_inc(x_17);
+x_18 = lean_ctor_get(x_16, 1);
+lean_inc(x_18);
+lean_dec(x_16);
+x_19 = lean_unsigned_to_nat(2u);
+x_20 = l_Lean_Syntax_getArg(x_1, x_19);
+x_21 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_21, 0, x_17);
+x_22 = 1;
+lean_inc(x_8);
+lean_inc(x_7);
+lean_inc(x_6);
+lean_inc(x_5);
+lean_inc(x_4);
+lean_inc(x_3);
+x_23 = l_Lean_Elab_Term_elabTerm(x_20, x_21, x_22, x_3, x_4, x_5, x_6, x_7, x_8, x_18);
+if (lean_obj_tag(x_23) == 0)
+{
+lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; 
+x_24 = lean_ctor_get(x_23, 0);
+lean_inc(x_24);
+x_25 = lean_ctor_get(x_23, 1);
+lean_inc(x_25);
+lean_dec(x_23);
+x_26 = l_Lean_Elab_Term_elabStateRefT___closed__2;
+x_27 = 0;
+x_28 = lean_box(0);
+lean_inc(x_5);
+x_29 = l___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl(x_26, x_27, x_28, x_5, x_6, x_7, x_8, x_25);
+x_30 = lean_ctor_get(x_29, 0);
+lean_inc(x_30);
+x_31 = lean_ctor_get(x_29, 1);
+lean_inc(x_31);
+lean_dec(x_29);
+x_32 = l_Lean_mkAppStx___closed__9;
+lean_inc(x_30);
+x_33 = lean_array_push(x_32, x_30);
+lean_inc(x_24);
+x_34 = lean_array_push(x_33, x_24);
+x_35 = l_Lean_Elab_Term_elabStateRefT___closed__4;
+lean_inc(x_8);
+lean_inc(x_7);
+lean_inc(x_6);
+lean_inc(x_5);
+x_36 = l_Lean_Meta_mkAppM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_isMonad_x3f___spec__1(x_35, x_34, x_3, x_4, x_5, x_6, x_7, x_8, x_31);
+if (lean_obj_tag(x_36) == 0)
+{
+lean_object* x_37; lean_object* x_38; lean_object* x_39; 
+x_37 = lean_ctor_get(x_36, 0);
+lean_inc(x_37);
+x_38 = lean_ctor_get(x_36, 1);
+lean_inc(x_38);
+lean_dec(x_36);
+lean_inc(x_8);
+lean_inc(x_7);
+lean_inc(x_6);
+lean_inc(x_5);
+lean_inc(x_4);
+lean_inc(x_3);
+x_39 = l_Lean_Elab_Term_mkInstMVar(x_37, x_3, x_4, x_5, x_6, x_7, x_8, x_38);
+if (lean_obj_tag(x_39) == 0)
+{
+lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; 
+x_40 = lean_ctor_get(x_39, 1);
+lean_inc(x_40);
+lean_dec(x_39);
+x_41 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoe___closed__3;
+x_42 = lean_array_push(x_41, x_30);
+x_43 = lean_array_push(x_42, x_13);
+x_44 = lean_array_push(x_43, x_24);
+x_45 = l_Lean_Elab_Term_elabStateRefT___closed__6;
+x_46 = l_Lean_Meta_mkAppM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_isMonad_x3f___spec__1(x_45, x_44, x_3, x_4, x_5, x_6, x_7, x_8, x_40);
+lean_dec(x_4);
+lean_dec(x_3);
+return x_46;
+}
+else
+{
+uint8_t x_47; 
+lean_dec(x_30);
+lean_dec(x_24);
+lean_dec(x_13);
+lean_dec(x_8);
+lean_dec(x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+x_47 = !lean_is_exclusive(x_39);
+if (x_47 == 0)
+{
+return x_39;
+}
+else
+{
+lean_object* x_48; lean_object* x_49; lean_object* x_50; 
+x_48 = lean_ctor_get(x_39, 0);
+x_49 = lean_ctor_get(x_39, 1);
+lean_inc(x_49);
+lean_inc(x_48);
+lean_dec(x_39);
+x_50 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_50, 0, x_48);
+lean_ctor_set(x_50, 1, x_49);
+return x_50;
+}
+}
+}
+else
+{
+uint8_t x_51; 
+lean_dec(x_30);
+lean_dec(x_24);
+lean_dec(x_13);
+lean_dec(x_8);
+lean_dec(x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+x_51 = !lean_is_exclusive(x_36);
+if (x_51 == 0)
+{
+return x_36;
+}
+else
+{
+lean_object* x_52; lean_object* x_53; lean_object* x_54; 
+x_52 = lean_ctor_get(x_36, 0);
+x_53 = lean_ctor_get(x_36, 1);
+lean_inc(x_53);
+lean_inc(x_52);
+lean_dec(x_36);
+x_54 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_54, 0, x_52);
+lean_ctor_set(x_54, 1, x_53);
+return x_54;
+}
+}
+}
+else
+{
+uint8_t x_55; 
+lean_dec(x_13);
+lean_dec(x_8);
+lean_dec(x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+x_55 = !lean_is_exclusive(x_23);
+if (x_55 == 0)
+{
+return x_23;
+}
+else
+{
+lean_object* x_56; lean_object* x_57; lean_object* x_58; 
+x_56 = lean_ctor_get(x_23, 0);
+x_57 = lean_ctor_get(x_23, 1);
+lean_inc(x_57);
+lean_inc(x_56);
+lean_dec(x_23);
+x_58 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_58, 0, x_56);
+lean_ctor_set(x_58, 1, x_57);
+return x_58;
+}
+}
+}
+else
+{
+uint8_t x_59; 
+lean_dec(x_8);
+lean_dec(x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+x_59 = !lean_is_exclusive(x_12);
+if (x_59 == 0)
+{
+return x_12;
+}
+else
+{
+lean_object* x_60; lean_object* x_61; lean_object* x_62; 
+x_60 = lean_ctor_get(x_12, 0);
+x_61 = lean_ctor_get(x_12, 1);
+lean_inc(x_61);
+lean_inc(x_60);
+lean_dec(x_12);
+x_62 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_62, 0, x_60);
+lean_ctor_set(x_62, 1, x_61);
+return x_62;
+}
+}
+}
+}
+lean_object* l_Lean_Meta_mkArrow___at_Lean_Elab_Term_elabStateRefT___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+_start:
+{
+lean_object* x_10; 
+x_10 = l_Lean_Meta_mkArrow___at_Lean_Elab_Term_elabStateRefT___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
+lean_dec(x_8);
+lean_dec(x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+return x_10;
+}
+}
+lean_object* l_Lean_Elab_Term_elabStateRefT___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+_start:
+{
+lean_object* x_10; 
+x_10 = l_Lean_Elab_Term_elabStateRefT(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_10;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("stateRefT");
+return x_1;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_mkAppStx___closed__6;
+x_2 = l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__3() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabStateRefT___boxed), 9, 0);
+return x_1;
+}
+}
+lean_object* l___regBuiltin_Lean_Elab_Term_elabStateRefT(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = l_Lean_Elab_Term_termElabAttribute;
+x_3 = l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__2;
+x_4 = l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__3;
+x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
 lean_object* initialize_Init(lean_object*);
 lean_object* initialize_Init_Data_ToString(lean_object*);
 lean_object* initialize_Lean_Compiler_BorrowedAnnotation(lean_object*);
@@ -16951,6 +17345,27 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabSubst___closed__1);
 res = l___regBuiltin_Lean_Elab_Term_elabSubst(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l_Lean_Elab_Term_elabStateRefT___closed__1 = _init_l_Lean_Elab_Term_elabStateRefT___closed__1();
+lean_mark_persistent(l_Lean_Elab_Term_elabStateRefT___closed__1);
+l_Lean_Elab_Term_elabStateRefT___closed__2 = _init_l_Lean_Elab_Term_elabStateRefT___closed__2();
+lean_mark_persistent(l_Lean_Elab_Term_elabStateRefT___closed__2);
+l_Lean_Elab_Term_elabStateRefT___closed__3 = _init_l_Lean_Elab_Term_elabStateRefT___closed__3();
+lean_mark_persistent(l_Lean_Elab_Term_elabStateRefT___closed__3);
+l_Lean_Elab_Term_elabStateRefT___closed__4 = _init_l_Lean_Elab_Term_elabStateRefT___closed__4();
+lean_mark_persistent(l_Lean_Elab_Term_elabStateRefT___closed__4);
+l_Lean_Elab_Term_elabStateRefT___closed__5 = _init_l_Lean_Elab_Term_elabStateRefT___closed__5();
+lean_mark_persistent(l_Lean_Elab_Term_elabStateRefT___closed__5);
+l_Lean_Elab_Term_elabStateRefT___closed__6 = _init_l_Lean_Elab_Term_elabStateRefT___closed__6();
+lean_mark_persistent(l_Lean_Elab_Term_elabStateRefT___closed__6);
+l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__1();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__1);
+l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__2();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__2);
+l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__3 = _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__3();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__3);
+res = l___regBuiltin_Lean_Elab_Term_elabStateRefT(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus
diff --git a/stage0/stdlib/Lean/Parser/Term.c b/stage0/stdlib/Lean/Parser/Term.c
index 105cb5db86..c3a14c603f 100644
--- a/stage0/stdlib/Lean/Parser/Term.c
+++ b/stage0/stdlib/Lean/Parser/Term.c
@@ -52916,7 +52916,7 @@ static lean_object* _init_l_Lean_Parser_Term_stateRefT___elambda__1___closed__5(
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("StateRefTNew");
+x_1 = lean_mk_string("StateRefT");
 return x_1;
 }
 }