diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v
index 600951aab25427f6d6a276a0872ccf7134565fe0..594bd361ae3c682fd694061ecc8c2d32f718c863 100644
--- a/iris/proofmode/string_ident.v
+++ b/iris/proofmode/string_ident.v
@@ -91,7 +91,10 @@ However, this function will produce wrong results under [Set Mangle Names], so
 use with caution. *)
 Ltac string_to_ident s :=
   let s := (eval cbv in s) in
-  let x := constr:(ltac:(StringToIdent.intros_by_string s; exact tt) : unit -> unit) in
+  let x := constr:(ltac:(clear; (* needed since s might already be in scope
+                         where this is called *)
+                         StringToIdent.intros_by_string s;
+                         exact tt) : unit -> unit) in
   match x with
   | (fun (name:_) => _) => name
   end.
diff --git a/tests/string_ident.ref b/tests/string_ident.ref
index 8486db4a4328db101b9a23c5080ba734d202bb7c..3ea77a67ebe207f5cc77ff5364ce0113edfaff84 100644
--- a/tests/string_ident.ref
+++ b/tests/string_ident.ref
@@ -10,3 +10,5 @@ Uncaught Ltac2 exception: StringToIdent.NotStringLiteral (constr:(4))
      : string
 The command has indeed failed with message:
 Uncaught Ltac2 exception: StringToIdent.NotStringLiteral (constr:(s))
+"test_string_to_ident_not_fresh"
+     : string
diff --git a/tests/string_ident.v b/tests/string_ident.v
index bc42e01062337d0f9b0f2e9f2a59124c2a87effc..6de14c131a30ca84cbf538d5ba5b7da36ae9abb9 100644
--- a/tests/string_ident.v
+++ b/tests/string_ident.v
@@ -26,3 +26,13 @@ Lemma test_not_literal (s:string) : ∀ (n:nat), True.
 Proof.
   Fail let x := fresh in intros x; rename_by_string x s.
 Abort.
+
+Check "test_string_to_ident_not_fresh".
+Lemma test_string_to_ident_not_fresh (n:nat) : ∀ (n:nat), nat.
+Proof.
+  (* we want to check that this [string_to_ident "n"] call succeeds even with
+  [n] in the context *)
+  let x := string_to_ident "n" in
+  let x := fresh x in
+  intros x.
+Abort.