diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 1f1804cb0e..b96221c018 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -12,7 +12,7 @@ namespace Simp
 builtin_initialize congrHypothesisExceptionId : InternalExceptionId ←
   registerInternalExceptionId `congrHypothesisFailed
 
-def throwCongrHypothesisFailed {α} : MetaM α :=
+def throwCongrHypothesisFailed : MetaM α :=
   throw <| Exception.internal congrHypothesisExceptionId
 
 def Result.getProof (r : Result) : MetaM Expr := do
diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 05fe2263e4..6b3cae8161 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -141,7 +141,7 @@ def rewriteUsingDecide? (e : Expr) : MetaM (Option Result) := withReducibleAndIn
     x
 
 @[inline] def tryUnfold (e : Expr) (x : SimpM Step) : SimpM Step := do
-  if e.isApp && e.getAppFn.isConst && (← read).toUnfold.contains e.getAppFn.constName! then
+  if e.getAppFn.isConst && (← read).toUnfold.contains e.getAppFn.constName! then
     -- TODO: try simp lemmas
     match (← withDefault <| unfoldDefinition? e) with
     | some eNew => return Step.visit { expr := eNew }
diff --git a/tests/lean/run/simp7.lean b/tests/lean/run/simp7.lean
index 2ce8cdb6a3..c5da87dc76 100644
--- a/tests/lean/run/simp7.lean
+++ b/tests/lean/run/simp7.lean
@@ -29,5 +29,11 @@ def head [Inhabited α] : List α → α
   | []   => arbitrary
   | a::_ => a
 
-theorem ex [Inhabited α] (a : α) (as : List α) : head (a::as) = a :=
+theorem ex4 [Inhabited α] (a : α) (as : List α) : head (a::as) = a :=
   by simp [head]
+
+def foo := 10
+
+theorem ex5 (x : Nat) : foo + x = 10 + x := by
+  simp [foo]
+  done