diff --git a/Aesop/BuiltinRules/DestructProducts.lean b/Aesop/BuiltinRules/DestructProducts.lean
index 9389f69a..fa14add3 100644
--- a/Aesop/BuiltinRules/DestructProducts.lean
+++ b/Aesop/BuiltinRules/DestructProducts.lean
@@ -50,7 +50,7 @@ private def destructProductHyp (goal : MVarId) (hyp : FVarId)
       goal.withContext $ check prf
       let [goal] ← goal.apply prf
         | throwError "destructProducts: apply did not return exactly one goal"
-      discard $ goal.introN (genHyps.size - 1)
+      let (_, goal) ← goal.introN (genHyps.size - 1)
       let (_, goal) ← goal.introN 2
       goal.clear hyp
 
diff --git a/AesopTest/DestructProducts.lean b/AesopTest/DestructProducts.lean
index 8b790d38..d5e0d870 100644
--- a/AesopTest/DestructProducts.lean
+++ b/AesopTest/DestructProducts.lean
@@ -43,3 +43,7 @@ example {p : α → Type} (h : Σ a, p a) : Sig α p := by
 
 example {p : α → Type} (h : Σ' a, p a) : Sig α p := by
   aesop
+
+-- Test case for a bug reported by Jakob von Raumer.
+example (x y : α × α) (h: p ∧ (x = y)) : x = y := by
+  aesop (simp_options := { enabled := false })