diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 3af7a37ccf69a4e7f486626cd143d0369df58687..8ddfcb423e4daebe6278e7887f4f1afb0fb7cb1f 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -94,6 +94,19 @@ Tactic failure: iExistDestruct: cannot destruct P.
   --------------------------------------â–¡
   P
   
+"test_iDestruct_exists_anonymous"
+     : string
+1 subgoal
+  
+  PROP : bi
+  P : PROP
+  Φ : nat → PROP
+  H : nat
+  ============================
+  "HΦ" : ∃ x : nat, Φ x
+  --------------------------------------∗
+  ∃ x : nat, Φ x
+  
 "test_iIntros_forall_pure"
      : string
 1 subgoal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 893a7e6a5fc71e0b67bb2f189740f01d1772d2ef..56aa97a8dc9efb0e3d2423f2d5afb5bcf187b14f 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -184,6 +184,18 @@ Proof.
   iExists y0; auto.
 Qed.
 
+(* regression test for #337 *)
+Check "test_iDestruct_exists_anonymous".
+Lemma test_iDestruct_exists_anonymous P Φ :
+  (∃ _:nat, P) ∗ (∃ x:nat, Φ x) -∗ P ∗ ∃ x, Φ x.
+Proof.
+  iIntros "[HP HΦ]".
+  (* this should not use [x] as the default name for the unnamed binder *)
+  iDestruct "HP" as (?) "$". Show.
+  iDestruct "HΦ" as (x) "HΦ".
+  by iExists x.
+Qed.
+
 Definition an_exists P : PROP := (∃ (an_exists_name:nat), ▷^an_exists_name P)%I.
 
 (* should use the name from within [an_exists] *)
diff --git a/theories/proofmode/ident_name.v b/theories/proofmode/ident_name.v
index c5886dcb0ab7345bf68c4d1731862c830d9faf2b..c79e67e81b893923a07b4ff0a1c16178b95fda7e 100644
--- a/theories/proofmode/ident_name.v
+++ b/theories/proofmode/ident_name.v
@@ -27,8 +27,11 @@ Arguments as_ident_name {A B f} name : assert.
 
 Ltac solve_as_ident_name :=
   lazymatch goal with
-  | |- AsIdentName (λ x, _) _ =>
-    let name := to_ident_name x in
+  (* The [H] here becomes the default name if the binder is anonymous. We use
+     [H] with the idea that an unnamed and unused binder is likely to be a
+     proposition. *)
+  | |- AsIdentName (λ H, _) _ =>
+    let name := to_ident_name H in
     notypeclasses refine (as_ident_name name)
   | _ => notypeclasses refine (to_ident_name __unknown)
   end.