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