chore: rebase on 2022-07-10

leanprover · Jul 11, 2022 · 680f66a · 680f66a
1 parent 8f6100e
commit 680f66a
Showing 1 changed file with 3 additions and 4 deletions.
diff --git 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