From 0824e6b22b38084ce7cd5cee9f232c7d9494454e Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Sun, 10 Jul 2022 21:43:53 -0400
Subject: [PATCH] chore: rebase on 2022-07-10

---
 src/Lean/Widget/UserWidget.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean
index b473937243..3c676a2ff5 100644
--- a/src/Lean/Widget/UserWidget.lean
+++ b/src/Lean/Widget/UserWidget.lean
@@ -7,6 +7,7 @@ Authors: E.W.Ayers
 import Lean.Widget.Basic
 import Lean.Data.Json
 import Lean.Environment
+import Lean.Elab.Eval
 import Lean.Server
 
 open Lean
@@ -145,10 +146,8 @@ def saveWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (widg
 
 syntax (name := widgetCmd) "#widget " ident term : command
 
-private unsafe def  evalJsonUnsafe (stx : Syntax) : TermElabM Json := do
-  let e ← Term.elabTerm stx (mkConst ``Json)
-  let e ← Meta.instantiateMVars e
-  Term.evalExpr Json ``Json e
+private unsafe def evalJsonUnsafe (stx : Syntax) : TermElabM Json := do
+  Term.evalTerm Json (mkConst ``Json) stx
 
 @[implementedBy evalJsonUnsafe]
 private opaque evalJson (stx : Syntax) : TermElabM Json