cleanup

leanprover-community · Jan 11, 2024 · f6e06a1 · f6e06a1
1 parent b4f86d7
commit f6e06a1
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/Aesop/Search/Expansion/Simp.lean b/Aesop/Search/Expansion/Simp.lean
@@ -9,6 +9,7 @@ import Aesop.Script
 import Aesop.RuleSet
 
 open Lean Lean.Meta
+open Lean.Elab.Tactic (mkSimpOnly)
 open Simp (UsedSimps)
 
 namespace Aesop
@@ -48,7 +49,7 @@ def mkNormSimpOnlySyntax (inGoal : MVarId) (normSimpUseHyps : Bool)
  MetaM Syntax.Tactic := do
  let originalStx ← mkNormSimpSyntax normSimpUseHyps configStx?
  let stx ← inGoal.withContext do
- Lean.Elab.Tactic.mkSimpOnly originalStx usedTheorems
+ mkSimpOnly originalStx usedTheorems
  return ⟨stx⟩
 
 def mkNormSimpContext (rs : RuleSet) (simpConfig : Aesop.SimpConfig) :