From 99bd215dcbfbc64a44b86f7c478b0f1f28018bb0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 12 Dec 2021 08:22:31 -0800
Subject: [PATCH] chore: `where` struct instance parser

The parser was modified to fix issue https://github.com/leanprover/lean4/issues/753

cc @tydeu
---
 Lake/DSL/Commands.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Lake/DSL/Commands.lean b/Lake/DSL/Commands.lean
index 49b0485b3c..5fbdec5566 100644
--- a/Lake/DSL/Commands.lean
+++ b/Lake/DSL/Commands.lean
@@ -30,7 +30,7 @@ syntax packageDeclTyped :=
   Term.typeSpec declValSimple
 
 syntax packageDeclSpec :=
-  ident (Term.whereDecls <|> packageDeclTyped <|> packageDeclWithBinders)?
+  ident (Command.whereStructInst <|> packageDeclTyped <|> packageDeclWithBinders)?
 
 scoped syntax (name := packageDecl)
 (docComment)? "package " packageDeclSpec : command