From 1f3919f08a3c18b796cc1674652fdc081e6188ba Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 30 Dec 2024 00:43:06 -0800
Subject: [PATCH] chore: add assertion

A global theorem should not have free variables in `symbols`.
---
 src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean b/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean
index 82833aad3671..4b605d38bef5 100644
--- a/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean
+++ b/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean
@@ -288,6 +288,7 @@ def addTheoremPattern (declName : Name) (numParams : Nat) (patterns : List Expr)
   let us := info.levelParams.map mkLevelParam
   let proof := mkConst declName us
   let (patterns, symbols, bvarFound) ← NormalizePattern.main patterns
+  assert! symbols.all fun s => s matches .const _
   trace[grind.pattern] "{declName}: {patterns.map ppPattern}"
   if let .missing pos ← checkCoverage proof numParams bvarFound then
      let pats : MessageData := m!"{patterns.map ppPattern}"