diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index b18be09973..4ecebdd9e5 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/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/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 42aa7bbc5b..2050bdd6e6 100644
--- a/src/Lean/Parser/Term.lean
+++ b/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