diff --git a/LeanCopilot/LlmAesop.lean b/LeanCopilot/LlmAesop.lean
index 2fa37f9..5af1840 100644
--- a/LeanCopilot/LlmAesop.lean
+++ b/LeanCopilot/LlmAesop.lean
@@ -1,10 +1,11 @@
 import LeanCopilot.Tactics
 import LeanCopilot.Options
+import Std.Data.String.Basic
 import Aesop
 
 set_option autoImplicit false
 
-open Lean
+open Lean Meta Elab Term Tactic
 
 namespace LeanCopilot
 
@@ -13,7 +14,18 @@ def tacGen : Aesop.TacGen := fun (mvarId : MVarId) => do
   let state ← ppTacticState [mvarId]
   let nm ← SuggestTactics.getGeneratorName
   let model ← getGenerator nm
-  generate model state ""
+  let suggestions ← generate model state ""
+  -- A temporary workaround to prevent the tactic from using the current theorem.
+  -- TODO: Use a more pincipled way, e.g., see Lean4Repl.lean in LeanDojo.
+  let theoremName := match (← liftM (m := MetaM) <| Term.TermElabM.run getDeclName?).1.get! |>.toString with
+    | "_example" => ""
+    | n => n
+  let theoremNameMatcher := String.Matcher.ofString theoremName
+  let filteredSuggestions := suggestions.filterMap fun ((t, s) : String × Float) =>
+    let isAesop := t == "aesop"
+    let isSelfReference := ¬ (theoremName == "") ∧ (theoremNameMatcher.find? t |>.isSome)
+    if isSelfReference ∨ isAesop then none else some (t, s)
+  return filteredSuggestions
 
 
 macro "#configure_llm_aesop" : command => `(@[aesop 100%] def tacGen := LeanCopilot.tacGen)
diff --git a/LeanCopilot/Models/FFI.lean b/LeanCopilot/Models/FFI.lean
index c6839aa..ae9d4b7 100644
--- a/LeanCopilot/Models/FFI.lean
+++ b/LeanCopilot/Models/FFI.lean
@@ -79,11 +79,7 @@ def generate (model : NativeGenerator) (input : String) (targetPrefix : String)
   let temperature := model.params.temperature
   let tokensWithScores := FFI.generate model.name inputTokens targetPrefixTokens numReturnSequences beamSize minLength maxLength lengthPenalty patience temperature
 
-  return tokensWithScores.filterMap fun ((ts, s) : Array String × Float) =>
-    match tokenizer.detokenize ts with
-    | "aesop" => none
-    | t => some (t, s)
-
+  return tokensWithScores.filterMap fun ((ts, s) : Array String × Float) => (tokenizer.detokenize ts, s)
 
 
 instance : TextToText NativeGenerator where
diff --git a/LeanCopilot/Tactics.lean b/LeanCopilot/Tactics.lean
index ba97cbd..a1760bc 100644
--- a/LeanCopilot/Tactics.lean
+++ b/LeanCopilot/Tactics.lean
@@ -2,8 +2,9 @@ import Lean
 import LeanCopilot.Options
 import LeanCopilot.Frontend
 import Aesop.Util.Basic
+import Std.Data.String.Basic
 
-open Lean Meta Elab Tactic
+open Lean Meta Elab Term Tactic
 
 set_option autoImplicit false
 
@@ -34,11 +35,23 @@ Generate a list of tactic suggestions.
 -/
 def suggestTactics (targetPrefix : String) : TacticM (Array (String × Float)) := do
   let state ← getPpTacticState
-  if ← isVerbose then
-    logInfo s!"State:\n{state}"
   let nm ← getGeneratorName
   let model ← getGenerator nm
-  generate model state targetPrefix
+  let suggestions ← generate model state targetPrefix
+  -- A temporary workaround to prevent the tactic from using the current theorem.
+  -- TODO: Use a more pincipled way, e.g., see Lean4Repl.lean in LeanDojo.
+  let theoremName := match (← getDeclName?).get! |>.toString with
+    | "_example" => ""
+    | n => n
+  let theoremNameMatcher := String.Matcher.ofString theoremName
+  if ← isVerbose then
+    logInfo s!"State:\n{state}"
+    logInfo s!"Theorem name:\n{theoremName}"
+  let filteredSuggestions := suggestions.filterMap fun ((t, s) : String × Float) =>
+    let isAesop := t == "aesop"
+    let isSelfReference := ¬ (theoremName == "") ∧ (theoremNameMatcher.find? t |>.isSome)
+    if isSelfReference ∨ isAesop then none else some (t, s)
+  return filteredSuggestions
 
 
 private def annotatePremise (premisesWithInfoAndScores : String × String × String × Float) : MetaM String := do
diff --git a/lake-manifest.json b/lake-manifest.json
index ec5e9eb..55b881e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "baf6defee1fe881ae535519c0776f37f6ef08603",
+   "rev": "b197bd218dbab248ad8899404334d41da04f5d13",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",