From 7da0dd2fcf68407d4cf066c1193908b24cb71124 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 17 Oct 2022 14:07:16 -0700
Subject: [PATCH] fix: remove `` `(funBinder|``

---
 Lake/DSL/DeclUtil.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Lake/DSL/DeclUtil.lean b/Lake/DSL/DeclUtil.lean
index adee1a5ae8..8f00843de0 100644
--- a/Lake/DSL/DeclUtil.lean
+++ b/Lake/DSL/DeclUtil.lean
@@ -52,6 +52,7 @@ syntax simpleBinder :=
   ident <|> bracketedSimpleBinder
 
 abbrev SimpleBinder := TSyntax ``simpleBinder
+open Lean.Parser.Term in
 def expandOptSimpleBinder (stx? : Option SimpleBinder) : MacroM FunBinder := do
   match stx? with
   | some stx =>