From 9519479726b57479fdaace3f84cf7472809b51ec Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Aug 2020 15:19:22 -0700
Subject: [PATCH] chore: fix test

---
 tests/lean/run/doNotation1.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/run/doNotation1.lean b/tests/lean/run/doNotation1.lean
index a32deb8392..c15310a2b2 100644
--- a/tests/lean/run/doNotation1.lean
+++ b/tests/lean/run/doNotation1.lean
@@ -2,7 +2,7 @@ open Lean
 
 partial def expandHash : Syntax → StateT Bool MacroM Syntax
 | Syntax.node k args =>
-  if k == `doHash then do set true; `(←MonadState.get)
+  if k == `doHash then do set true; `(←HasGet.get)
   else do
     args ← args.mapM expandHash;
     pure $ Syntax.node k args