diff --git a/src/Lean/Meta/Tactic/Simp/SimpAll.lean b/src/Lean/Meta/Tactic/Simp/SimpAll.lean
index d5796608bd..cca35ef593 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpAll.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpAll.lean
@@ -56,12 +56,21 @@ private partial def loop : M Bool := do
     | none => return true -- closed the goal
     | some (proofNew, typeNew) =>
       unless typeNew == entry.type do
-        let id ← mkFreshUserName `h
-        let simpThmsNew ← (← getSimpTheorems).add #[] proofNew (name? := id)
+        /- The theorem for the simplified entry must use the same `id` of the theorem before simplification. Otherwise,
+           the previous versions can be used to self-simplify the new version. For example, suppose we have
+           ```
+            x : Nat
+            h : x ≠ 0
+            ⊢ Unit
+           ```
+           In the first round, `h : x ≠ 0` is simplified to `h : ¬ x = 0`. If we don't use the same `id`, in the next round
+           the first version would simplify it to `h : True`.
+        -/
+        let simpThmsNew ← (← getSimpTheorems).add #[] proofNew (name? := entry.id)
         modify fun s => { s with
           modified         := true
           ctx.simpTheorems := simpThmsNew
-          entries[i]       := { entry with type := typeNew, proof := proofNew, id := id }
+          entries[i]       := { entry with type := typeNew, proof := proofNew, id := entry.id }
         }
   -- simplify target
   let mvarId := (← get).mvarId
diff --git a/tests/lean/1027.lean b/tests/lean/1027.lean
new file mode 100644
index 0000000000..a67a64f853
--- /dev/null
+++ b/tests/lean/1027.lean
@@ -0,0 +1,4 @@
+example (h : x ≠ 0) : Unit := by
+  simp_all
+  trace_state
+  sorry
diff --git a/tests/lean/1027.lean.expected.out b/tests/lean/1027.lean.expected.out
new file mode 100644
index 0000000000..d9591e0818
--- /dev/null
+++ b/tests/lean/1027.lean.expected.out
@@ -0,0 +1,4 @@
+x : Nat
+h : ¬x = 0
+⊢ Unit
+1027.lean:4:2-4:7: warning: declaration uses 'sorry'